Towards a migration guide: TLA+ Toolbox → TLA+ VSCode extension

[Markus Kuppe]

Hi everyone,

for those of you who have switched from the TLA+ Toolbox to the TLA+ VS Code extension — and are enjoying it — the TLA+ project could really use your help!

We would like to create a migration guide to help others make the transition smoothly. As discussed in GitHub issue #423 [1], most of the current beginner documentation still depends heavily on the Toolbox. Since the Toolbox is now mostly in maintenance mode, that documentation is sending new TLA+ users down the legacy path.

The two environments are largely equivalent in features, but active development and improvements are now focused on the VS Code extension. In addition, VS Code offers native support for AI tools and coding assistants, which can make learning and using TLA+ more efficient and approachable.

If you have already made the move, your experience — what worked well, what caused confusion, and what you wish you had known — would be extremely valuable to others in the community.

We will use the GitHub issue to organize the work.

Thanks,
Markus

[1] https://github.com/tlaplus/vscode-tlaplus/issues/423