# The TLA+ Toolbox

arXiv: https://arxiv.org/abs/1912.10633 · HTML: https://mlsanity.com/paper/1912.10633/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Dec 2019.

## Built on by (most cited first, 3 of 3)

- [Federated Learning for Cyber Physical Systems: A Comprehensive Survey](https://mlsanity.com/paper/2505.04873/) (2025)
- [ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair](https://mlsanity.com/paper/2602.12058/) (2026)
- [Specula: Scaling formal specifications for autonomous model checking of system code](https://mlsanity.com/paper/2607.25333/) (2026)

## Abstract (arXiv)

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.