This section contains the tools available for download for the TLA+ specification language and the PlusCal
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.
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.