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.
http://lamport.azurewebsites.net/tla/tla.html
http://lamport.azurewebsites.net/tla/hyperbook.html
http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-spec-tla-plus.pdf