Started work on specifying layer two bitcoin contracts using TLA+. The first goal is of course LN. However, writing LN contracts first requires specifying a bitcoin transactions module.

Repo: https://github.com/pool2win/bitcoin-contracts-tlaplus
BitcoinTransactions module: https://github.com/pool2win/bitcoin-contracts-tlaplus/blob/main/BitcoinTransactions.pdf
LNContracts module (soon to start using BitcoinTransactions module): https://github.com/pool2win/bitcoin-contracts-tlaplus/blob/main/LNContracts.pdf

I'll keep you posted on the progress. We already have the commitment transactions speced and next step is to spec the HTLC outputs in the commitment transactions.