search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.29k stars 200 forks source link

Fixed proofs in bcastByz #41

Closed banhday closed 3 years ago

banhday commented 3 years ago

It follows the changes mentioned in #40. I added additional proof steps in theorems related to the inductive invariants TypeOK and FCConstraints. The updated proofs were checked with TLAPS version 1.4.5.