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.