The TLA+ Toolbox
This work addresses the needs of engineers using formal methods in industry, though it is incremental as it builds on the existing TLA+ Toolbox.
The paper tackles the challenge of scaling and debugging formal specifications in industry by introducing two novel features in the TLA+ Toolbox: CloudTLC for cloud-based model checking and a Profiler to debug inefficiencies and state space explosion.
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.