List of specifications in TLA+:
- P2P Broadcast
- Shamir Secret Sharing
- Miner share accounting and block generation We specify how broadcast shares are accounted for towards miner payouts. When a bitcoin block is found, all unaccounted for shares are added to miners Unspent Hasher Payout (UHPO). We do not spec out how the distributed key generation algorithm is run - instead we replace the public key for coinbase payout to simply be the concatenation of the miner id.
- The above spec for block generation uses the Bitcoin Transactions spec. The transaction spec uses a simple scriptSig = scriptPubkey check.
List of protocols still to be specified:
- Pedersen’s DKG using the P2P Broadcast
- Block coinbase and UHPO transaction constructions
- Generating threshold signature to update UHPO transactions
- Miner cash out protocol