TLA+ | The way to specify

There are various tools available for the TLA+ specification language and PlusCal algorithm language, as described in the Tools section in more detail. An additional tool is coming soon: the TLA+ Toolbox.

There are a number of existing tools for working on TLA+ specifications, the most important of which is the TLC model-checker. Although the proof side of TLA+ is not well-developed yet, with no proof tools and an incomplete definition of the proof language, TLA+ has already proved its worth in significant projects in hardware design, [...]

This tutorial describes the command line switches accepted by the console-based TLA+ Tools: SANY, TLC, and the PlusCal Translator. Most users will run the tools from the Toolbox, in which case the switches for SANY and TLC are irrelevant. When running the Toolbox, command line switches for the PlusCal translator can be provided in a [...]

This tutorial provides a description of the installation procedure of the console-based version of TLA+ Tools. Separate directions for completing the installation on Windows and on Unix are provided.