TLA+ Toolbox
A macOS IDE for TLA+ tools, with specification editing, PlusCal translation, TLC model checking, trace exploration, and proof-system support.
About
TLA+ Toolbox is an integrated development environment for working with TLA+ tools. It helps you create and edit specifications, inspect parsing errors in their source modules, and run PlusCal translation with translation errors marked in the code.
Key capabilities include:
- View pretty-printed versions of modules.
- Run the TLC model checker and explore its error traces, including evaluating formulas at trace steps.
- Run the TLA+ proof system.
Install with brew install --cask tla+-toolbox. This cask installs the TLA+ Toolbox.app application in /Applications. The supplied macOS download is an x86_64 build and the cask requires Rosetta. Consult the Toolbox welcome screen and help pages to get started.
The pdflatex program is needed only if you want to use the Toolbox’s PDF output command for pretty-printed modules; it is provided by a LaTeX installation. The Toolbox is an IDE for the TLA+ tools, not a general-purpose editor.
Sources: TLA+ Toolbox · Homebrew cask
New What’s new in 1.7.4 Aug 5, 2024 · OpenNavo editorial
- TLCFixes missed property violations in multi-worker liveness checking.