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
Getting started
Start the Toolbox, create your first specification in PlusCal, run TLC and have it verify a (safety) property.