The TLA+ Toolbox

Markus Alexander Kuppe
(Microsoft Research)
Leslie Lamport
(Microsoft Research)
Daniel Ricketts
(Oracle Corporation)

We discuss the workflows supported by the TLA+ Toolbox to write and verify specifications. We focus on features that are useful in industry because its users are primarily engineers. Two features are novel in the scope of formal IDEs: CloudTLC connects the Toolbox with cloud computing to scale up model checking. A Profiler helps to debug inefficient expressions and to pinpoint the source of state space explosion. For those who wish to contribute to the Toolbox or learn from its flaws, we present its technical architecture.

In Rosemary Monahan, Virgile Prevosto and Jose Proença: Proceedings Fifth Workshop on Formal Integrated Development Environment (F-IDE 2019), Porto, Portugal, 7th October 2019, Electronic Proceedings in Theoretical Computer Science 310, pp. 50–62.
Published: 23rd December 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: