TLA+ Toolbox

TLA+ is a high-level language for modeling programs and systems. It is useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.

The TLA Toolbox is an IDE (integrated development environment) for the TLA+ tools. Use it to:

Create and edit your specs, with the locations of parsing errors

marked in the modules

Run the PlusCal translator, with the locations of translation

errors marked in the PlusCal code

View the pretty-printed versions of your modules

Run the TLC model checker.

The Toolbox allows you to explorer an error trace produced by

TLC—for example, by evaluating arbitrary formulas at each step

in the trace

Run the TLA+ proof system