Most users of TLA+ will run the TLA+ tools from the TLA+ Toolbox. How to download them and run them outside the Toolbox is explained here.
SANY Syntactic Analyzer [show]
A parser and syntax checker for TLA+ specifications. It catches parsing errors and some
semanticerrors such as priming an expression containing primed variables. It was written by Jean-Charles Grégoire, David Jefferson, and Yuan Yu.
TLC Model Checker [show]
A model checker and simulator for
executableTLA+ specifications, which include most specifications written by engineers. It is an explicit-state model checker that can check both safety and liveness properties. For safety checking, TLC achieves an approximately linear speedup on modern large computers using 32 or more cores. It can further speed up model checking by running on a network of computers, and provides easy deployment on cloud systems. TLC was written by Yuan Yu and extended by Markus Kuppe.
Apalache Model Checker [show]
Apalache is an alternative to TLC for checking TLA+ specifications. While TLC is an explicit-state model checker, Apalache is a symbolic model checker. It checks safety for bounded executions and inductive invariants for unbounded executions, assuming that all data structures are finite. The tool leverages the SMT solver Z3, from Microsoft Research.
Apalache is still experimental, so be prepared to use the command-line and to help us discover bugs. TLA+ enthusiasts may find this model checker efficient, for example, when their spec contains many constraints over integers. The first version of Apalache was developed by Igor Konnov, Jure Kukovec and Thanh Hai Tran at TU Wien and Inria Nancy. Apalache is actively developed at Informal Systems by Shon Feder, Igor Konnov, Jure Kukovec, Gabriela Mafra, Rodrigo Otoni, and Thomas Pani.
PlusCal Translator [show]
A translator from the PlusCal algorithm language to TLA+. It was written by Keith Marzullo and the author of this web page.
TLAPS Proof System [show]
A system for mechanically checking proofs written in TLA+, including proofs of the kinds of properties described here. It is being developed at the Microsoft Research–Inria Joint Centre. See the TLAPS home page for more information. The first version of TLAPS was written by Kaustuv Chaudhuri. Improvements have been made by Damien Doligez, Stephan Merz, Hernán Vanzetto, Tomer Libal, Martin Riener, and Denis Cousineau.
TLATeX Pretty-Printer [show]
A program for typesetting TLA+ specifications. It is used by the Toolbox's Produce PDF Version command to generate and display a pdf file with a pretty-printed version of a specification. Chapter 13 of Specifying Systems has some tips on formatting this version. TLATeX can also be used outside the Toolbox to include TLA+ formulas and PlusCal code as part of a LaTeX document. Click here to find out how to run TLATeX outside the Toolbox. Here are instructions for how to include TLA+ formulas and PlusCal code in a LaTeX document. You will have to download the
The current versions of the language and tools differ somewhat from the ones described in the book. Most notably, language constructs for writing proofs have been added to TLA+, and a number of features have been added to TLC. All significant changes to the tools since the book was written are described in the document Current Versions of the TLA+ Tools, which contains a complete list of TLC command-line options. Changes to the language are described in this web page.
Known bugs in the tools are reported on the TLA+ Github issues page. Requests for additional features are also posted there. Tell us about any problems or inadequacies you find with the tools. But please remember that we are a small number of people trying to respond to the needs of an ever-growing number of users.