A TLA+ Proof System
- Kaustuv Chaudhuri ,
- Damien Doligez ,
- Leslie Lamport ,
- Stephan Merz
Proceedings of the LPAR Workshops, CEUR Workshop |
This is a description of the TLA+ constructs for writing formal proofs, and a preliminary description of the TLA proof system. It includes an appendix with a formal semantics of TLA+ proofs.