TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF