tla+rust - Writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+. BlockingQueue - Tutorial-style talk "Weeks of debugging can save you hours of TLA+". APALACHE - Symbolic model checker for TLA+. TLA+ Examples - Collection of TLA+ specifications of varying complexities. TLA+ Community Modules - TLA+ snippets, operators, and modules contributed and curated by the TLA+ community. TLC - Explicit state model checker for specifications written in TLA+.