TLA+ Conference
September 30, 2021
St. Louis, MO, USA

Interactive TLA+

Jesse Davis & Samy Lanka

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:

  • PrintT operator
  • Error traces and trace expressions
  • Graphviz output
  • TLA+ Graph Explorer
  • TSViz / ShiViz
  • Debugger in TLA+ for Visual Studio Code

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.