Home

High-Level View

News

Industrial Use

Learning

The Toolbox

Tools

Advanced Topics

More Stuff

ccc

TLA+ Tools

Leslie Lamport

Last modified on 18 March 2022


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.

The Tools

SANY Syntactic Analyzer       [show]

TLC Model Checker       [show]

Apalache Model Checker       [show]

PlusCal Translator       [show]

TLAPS Proof System       [show]

TLATeX Pretty-Printer       [show]

Documentation

Except for the PlusCal translator and TLAPS, the tools are described in the book Specifying Systems.   Documentation of the PlusCal translator can be found here.  Some documentation of the TLAPS proof system can be found on its web site and in the TLA+ Hyperbook.

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.