TLA+: Forking cases for tendermint #496
Conversation
There was a problem hiding this comment.
The spec looks very nice! The only thing that is not clear to me is what is expected as a result from model checking. I see a lot of files with counterexample in their name, and assume that we expect to see counterexamples. It would be nice if it this is explained in the README, as well as when submitting the pull request.
| \* the type of message records | ||
| MT == [type |-> STRING, src |-> STRING, round |-> Int, | ||
| proposal |-> STRING, validRound |-> Int, id |-> STRING] | ||
|
|
There was a problem hiding this comment.
Some comments on what the message record fields encode would be useful. For example, it is not clear that src is a process ID or that proposal is one of "PROPOSAL", "PREVOTE", "PRECOMMIT". Not sure if this is the appropriate place, maybe they can go in the file where the invariants are defined.
There was a problem hiding this comment.
Right. This will change with the new type checker anyways.
Co-authored-by: istoilkovska <[email protected]>
Co-authored-by: istoilkovska <[email protected]>
Co-authored-by: istoilkovska <[email protected]>
josef-widder
changed the title
This is the PR moved from the verification repository.
It contains a TLA+ specification of Tendermint consensus that is tuned to safety and fork scenarios.