TLA+ is a high-level, math-based, formal specification language used at companies such as Amazon and Microsoft to verify designs of distributed and concurrent systems. TLA+ specifications are written with the publicly available TLA+ Toolbox and verified by tools run from it. Those tools include a model checker and a proof system that can be used together on the same spec.

The paper discusses the rationale and drawbacks of the Toolbox's main features. Specifically, it reports on two Toolbox features which — to the best of our knowledge — are novel in the scope of formal IDEs: CloudTLC connects the Toolbox with cloud computing to scale up model checking. Moreover, CloudTLC allows to verify large numbers of models concurrently which enables users to explore a specification's design space faster. The expressiveness of TLA+ results in stated expressions that present a challenge for the model checker to evaluate efficiently. To address this challenge, the Toolbox provides a Profiler to analyze the evaluation to override inefficient expressions with efficient ones. We provide a summary about the Toolbox's architecture and its test infrastructure to show how others can add new features. The paper concludes with outlining future research and engineering-related work.