TLA+
Notes
Links
- Learn TLA+ (HN) (Intro) (HN) (Code) (Lobsters) (HN)
- TLA+ Proof Manager - General-purpose formal specification language that is particularly useful for describing concurrent and distributed systems. (Web)
- 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+. (Web)
- 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
- TLA+ Action Properties (2021)
- HN: TLA+ (2021)
- TLA+ Graph Explorer - Static web application to explore and animate a TLA+ state graph.
- Dr. TLA+ Series - Learn an algorithm and protocol, study a specification.
- PlusPy - Python interpreter for TLA+ specifications.
- Scaffolding TLA+ (2021)
- Specification Refinement (2021)
- tlacli - CLI tool for TLA+.
- Current and Future Tools for Interactive TLA+ (2021)
- TLA+ Conf 2021 (Videos)
- PlusCal Tutorial
- Using Abstract Data Types in TLA+ (2021)
- Ask HN: Do you use TLA+? (2022)
- TLA+ Animation Module - TLA+ module for animating TLC traces.
- TLA+ REPL - Simple REPL for the TLA+ language, using the TLC model checker.
- TLA+ Web UI Prototype
- TLA+ Transmutation - Elixir code generation from TLA+ specifications.
- Thinking about protocols with TLA+ and Apalache
- Azure Cosmos TLA+ specifications
- State Machines in TLA+
- Pirouette - Semi-automatic code extraction tool. It extracts a TLA+ specification from a Plutus Mealy Machine.
- TLA+ in TiDB
- Dockerfile for building the TLA+ tools
- modelator-py - Utilities for the TLA+ ecosystem and model-based testing using TLA+.
- TLA Sequence Diagram - Generate (message) sequence diagrams from TLA+ state traces.
- TLA+ Specification of Flexible Paxos
- Fixing a MongoDB Replication Protocol Bug with TLA+ (2019)
- TLA+ Video Course (2021)
- Using TLA+ to understand Xen vchan (2019) (Code)
- VSCode TLA+
- Tree-sitter grammar for TLA+
- ewd998 - Distributed termination detection on a ring, due to Shmuel Safra.
- TLA in Coq
- Writing a TLA⁺ tree-sitter grammar: my foray into free software (2023) (Lobsters)
- Creatively Misusing TLA+ (2023)
- TLA+ questions, answers, and experiments
- endive - Tool for inferring inductive invariants of protocols specified in TLA+.
- The Capability-Tractability Tradeoff (2023)
- An Introduction to TLA+ and Its Use in Parties (2023)
- Optimizing TLA+ Model Checking
- Going Beyond an Incident Report with TLA+ (2023)