TLA+ Toolbox

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

Users who would prefer a more lightweight IDE for TLA+ may want to try the Visual Studio Code extension for TLA+. However, it lacks many of the Toolbox's features.

• Official page: https://lamport.azurewebsites.net/tla/toolbox.html
• Download: https://github.com/tlaplus/tlaplus/releases/latest

Start the Toolbox, create your first specification in PlusCal, run TLC and have it verify a (safety) property.