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.
The current version of TLAPS is 1.4.5. It can (and should) be used from the Toolbox IDE. TLAPS is free software, distributed under the BSD license. You can obtain it in the download section.
New users should read the tutorial. The TLA+ hyperbook has a more in-depth tutorial of TLA+ and associated tools. The complete specification of the proof language is contained in the TLA+2 Preliminary Guide. You can also look at academic publications.
TLAPS is developed as part of the Tools for Proofs project at the Microsoft Research–Inria joint centre in Paris, France. Users are encouraged to use the TLA+ users Google group to discuss the system. A public bug-tracker is available.
This page can be found by
searching the Web for the 16-letter
string uidtlapshomepage.
Please do not put this string in any document that could wind up on
the Web--including email messages and Postscript and Word documents.
You can refer to it in Web documents as "the string obtained by
removing the - from uid-tlapshomepage".