Migrating from TLA+ Toolbox

TLA+ Toolbox is an IDE based on Eclipse, and for a long time it has been the official environment to work with TLA+ tools. See: https://lamport.azurewebsites.net/tla/toolbox.html

Since around 2020 the development focus has moved to improve the VScode plugin experience. The TLA+ Toolbox has now moved to archived mode. The current bugs won't be fixed and as as dependency rots, eventually it will stop being distributed as well. Therefore it is not recommended for daily use.

If you haven't yet, you should consider moving to the VSCode official extension:

• Don't need a separated IDE to work on TLA+
• Extension updates in almost real time without extra steps
• Matched feature set: we even have TLAPS integrated.
• Developers ready to take your feature requests and feedback.
• Native support for AI tools and coding assistants, which can make learning and using TLA+ more efficient and approachable.

Feel free to update this page with missing or useful information as you see fit. These are some ideas if you'd like to contribute:

• Quotes or short notes from users who migrated (was it easy/hard? Anything you think it's still missing?)
• "What I wish I knew"
• Example workflow improvements (e.g., using GitHub Copilot to write PlusCal)

We value feedback a lot. * If you have suggestions on how to improve this structure of this guide, please use: https://github.com/tlaplus/vscode-tlaplus/issues/423#issuecomment-3391933491 * If you have suggestions on how to improve the extension, create a new issue on https://github.com/tlaplus/vscode-tlaplus