  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.
