TLC is a tool in the TLA+ Toolbox that will model check a TLA+ specification. A high-level intuitive understanding of how this happens may make it easier to understand how to write useful TLA+ specs, so I’m documenting it here.

Disclaimer: I am not a TLA+ expert. This blog is largely for my own benefit and I will probably tell you lies.

A diagram showing how TLA+ specs are model checked by TLC