Learning TLA+ is a challenge for industrial programmers, who are accustomed to exploring their code’s behavior with a debugger and print statements, more than reasoning about it like mathematicians. Subtle mistakes in a specification can lead to a trivially-true specification. As Leslie Lamport says, “Always be suspicious of success.” Specifiers can catch such mistakes by exploring the spec’s behavior interactively, and they can gain a more intuitive understanding of TLA+.
This presentation is a survey of tools for interacting with TLA+, with guidance about which is best to use for which purpose. We will demonstrate:
Finally, we’ll propose a vision for the future of interactive TLA+ spec development: which features are most important and how they can be consolidated into one tool.