TLA+ | The way to specify

Tools

This section contains the tools available for download for the TLA+ specification language and the PlusCal algorithm language.

TLA Toolbox

The TLA Toolbox is a complete integrated development environment for writing, type-setting and model-checking specifications. It integrates the TLA Tools (SANY, TLATeX, TLC, PlusCal Translator, and the TLAPS proof system) with a single graphical interface.

TLA Tools

Even though the TLA Toolbox has mostly replaced the old way of using the TLA Tools, there are still some reason you might want to use the tools by themselves–for example, as part of an automated checking process. This section lets you download the tools separately.