2 ms·
This is the coolest demonstration of TLA+ I've seen to date. It takes you through specification, implementation, model-checking with TLC, visualization and anim
by pron 7y ago
This is the coolest demonstration of TLA+ I've seen to date. It takes you through specification, implementation, model-checking with TLC, visualization and animation, checking an inductive invariant, deductive proofs mechanically checked by TLAPS, refinement mapping and even model-based trace checking.
- fizwhiz 7y agoOT: I don't know if this level of rigor is employed by any major libraries. I know AWS has used it a great deal for their systems though notably recently[1] [1] https://assets.amazon.science/c4/11/de2606884b63bf4d95190a3c2390/millions-of-tiny-databases.pdf https://assets.amazon.science/c4/11/de2606884b63bf4d95190a3c...