Menu

About

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 distributedsystems. 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.

Get it

The current version of TLAPS is 1.0 (January 2012). 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.

Documents

New users should read the tutorial. The TLA+ hyperbook has a more indepth 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.

Community

TLAPS is developed as part of the Tools for Formal Specifications and for Proofs project at the Microsoft Research–INRIA joint centre in Saclay, France. Users are encouraged to use the TLAPS users mailing list to discuss the system. A public bug-tracker is available, courtesy of INRIA GForge.

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".