TLA+

Links

• TLA+ guide (HN)

• tla+rust - Writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+.

• Practical TLA+ by Hillel Wayne (2018) (Code)

• Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch (2019) (HN)

• TLA+ model checking made symbolic (2019) (HN)

• The TLA+ Toolbox (2019)

• BlockingQueue - Tutorial-style talk "Weeks of debugging can save you hours of TLA+".

• APALACHE - Symbolic model checker for TLA+.

• TLA+ Model Checking Made Symbolic (2019)

• TLA+ Examples - Collection of TLA+ specifications of varying complexities.

• Using TLA+ in the Real World to Understand a Glibc Bug (2020) (HN)

• Safety and Liveness Properties (2020)

• TLA+ at Microsoft to build planetary-scale systems (2020) (HN)

• TLA+ Community Event & Conference

• Modeling TLA+ in Z3Py (2020)

• Weeks of Debugging Can Save You Hours of TLA+ (2020)

• 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+.

• The TLA+ Home Page