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 PlusCal Translator.
The command line switches are detected, by the fact that they begin with a ‘-’ character. Once the first command line element that is not a switch is encountered, the rest are presumed to be file names.

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.