The TLA+ Proof System (TLAPS) mechanically checks TLA+ proofs. TLA+ is a general-purpose formal specification language that is particularly useful for describing concurrent and distributed systems. The TLA+ proof language is declarative, hierarchical, and scalable to large system specifications. It provides a consistent abstraction over the various “backend” verifiers. The current release of TLAPS does not perform temporal reasoning, and it does not handle some features of TLA+. See the list of currently unsupported TLA+ features. An extension to the full TLA+ language is under active development. However, TLAPS is now suitable for verifying safety properties of non-trivial algorithms. (Only trivial temporal-logic reasoning that is easily checked by hand is needed for safety.) For examples, see the proof of a Byzantine Paxos algorithm and the proof of a security architecture.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Cousineau, Denis; Doligez, Damien; Lamport, Leslie; Merz, Stephan; Ricketts, Daniel; Vanzetto, Hernán: TLA$^ + $ proofs (2012)
- Lamport, Leslie: How to write a 21$^\textst$ century proof (2012)
- Merz, Stephan; Vanzetto, Hernán: Automatic verification of TLA$^ + $ proof obligations with SMT solvers (2012)
- Akhtar, Sabina; Merz, Stephan; Quinson, Martin: A high-level language for modeling algorithms and their properties (2011)
- Lamport, Leslie: Checking a multithreaded algorithm with $^+$CAL (2007)
- Lamport, Leslie: Fast Paxos (2006)
- Joshi, Rajeev; Lamport, Leslie; Matthews, John; Tasiran, Serdar; Tuttle, Mark; Yu, Yuan: Checking cache-coherence protocols with TLA$^+$ (2003)
- Lamport, Leslie: Specifying concurrent systems with TLA$^+$ (1999)
Further publications can be found at: https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Publications.html