a specification of blockchain for liteclient and accountability

informalsystems / verification

Specifications of the protocols and the experiments on their verification

9 stars 2 forks source link

a specification of blockchain for liteclient and accountability #2

Closed konnov closed 4 years ago

konnov commented 5 years ago

This is a specification of the Tendermint blockchain and of its failure model that @josef-widder and I tuned for the lite client and fork accountability. It would be great to have comments on Blockchain.tla before we jump into a more involved spec of the lite client.

konnov commented 4 years ago

Thanks for the comments! I think I have addressed all issues. Will merge this PR and continue with PR #4, which also contains Blockchain.tla.