README
Awesome TLA+ 
TLA+ is a formal specification and verification language to help engineers design, specify, reason about, and verify complex software and hardware systems. It is widely used to verify the algorithms in distributed systems.
Contents
- WebSites
- Discussions
- Users
- Tools
- Books
- TLA+ blog posts and articles
- Real-world specs
- TLA+ Video Resources
- Scientific papers
- (University) courses teaching (with) TLA+
WebSites
- Homepage: http://www.tlapl.us (https://lamport.azurewebsites.net/tla/tla.html)
- TLA+ Project: https://project.tlapl.us (https://github.com/tlaplus)
- TLA+ Community Modules: https://modules.tlapl.us/ (https://github.com/tlaplus/CommunityModules)
- TLA+ Examples: https://examples.tlapl.us (https://github.com/tlaplus/Examples)
- Learn TLA+ (PlusCal): https://learntla.com/
- Writing Specs: https://writingspecs.com/ — Beginner-friendly intro to writing specs and TLA+ concepts; WIP, not comprehensive.
Discussions
- google groups: https://groups.google.com/forum/#!forum/tlaplus
- reddit: https://www.reddit.com/r/tlaplus/
- twitter: https://twitter.com/tlaplus
- stackoverflow: https://stackoverflow.com/questions/tagged/tla%2b
Users
- Microsoft
- Atomix
- Informal Systems: TLA+ for protocol specification, model checking, model-based testing, and security audits of blockchains
- Open Networking Foundation
- Zilliqa Research
- TLA+ Foundation Industry page
Tools
Verification
- TLC: https://tools.tlapl.us (https://github.com/tlaplus/tlaplus)
- TLAPM: https://proofs.tlapl.us (https://github.com/tlaplus/tlapm)
- Apalache: https://apalache.informal.systems/
Experimental
IDEs
- VSCode-extension: https://github.com/tlaplus/vscode-tlaplus
- Toolbox (Eclipse based IDE): https://tools.tlapl.us (https://github.com/tlaplus/tlaplus) (no longer maintained)
- Jupyter notebook: https://github.com/kelvich/tlaplus_jupyter
- Emacs mode: https://github.com/ratish-punnoose/tla-mode
- Another Emacs mode: https://git.sdf.org/bch/tlamode/
- Intellij IDEA plugin: https://github.com/ocadaruma/tlaplus-intellij-plugin
- Web-based tool for exploring, visualizing, and sharing formal specs: https://github.com/will62794/spectacle
- Web-based learning platform: https://learning.tlapl.us
Misc
- Specula: https://github.com/specula-org/Specula/
- Better-comments (VSCode): https://github.com/alygin/better-comments
- TLC command-line wrapper: https://github.com/pmer/tla-bin
Parsers
- SANY (Syntactic Analyzer): A parser and syntax checker for TLA+ specifications
- TLAPS: A system for mechanically checking proofs written in TLA+
- tree-sitter-tlaplus: A tree-sitter grammar for TLA⁺ and PlusCal
- tlapy: A collection of Python tools for working with TLA+ specifications
Books
- Specifying Systems (freely available)
- Hyperbook (freely available)
- Practical TLA+
- TLA+ in Practice and Theory (freely available)
TLA+ blog posts and articles
| name | description |
|---|---|
| AWS and TLA+ | Use of Formal Methods at Amazon Web Services |
| Batch Installer | Sending async batches of commands. |
| Redux | Redux reducers with verifying a temporal property. |
| Zero Downtime Deployments | A simple model of a deploying new code to servers where at least one server is always available to clients, and all available servers show the same code version. |
| Trading Algorithm | Trading boths executing trades in a simulated market, showing how it’s susceptible to flash crashes. |
| Detecting Linked-List Cycles | Finding cycles in linked lists. |
| Replicated Storage | Replicated storage system with a quorum. |
| Rate Limiter | Independent workers hitting a rate-limited API. |
| Thread Pool | Multiple reader and writer threads sharing a bounded queue, discovering deadlocks. |
| Bank Transfer | Specifying a bank transfer with overdraft protection. |
| Finding bugs in systems through formalization | Ensuring distributed jobs go from “pending” to “completed”. |
| Building A "Simple" Distributed System | Rebalanser - distributed resource allocation library. |
| Train Sidings – A TLA+ Example | Railroad line where two trains can pass each other. |
| Azure Cosmos TLA+ specifications | The consistency levels offered by Azure Cosmos DB (also see Murat Demirbas' talk). |
| Modeling Streamlet in TLA+ | A PlusCal spec of a crash fault-tolerant variant of the Streamlet blockchain protocol. |
| Understanding Apache Hudi's Consistency Model | TLA+ specification and model checking of Hudi's consistency model |
| Using TLA+ in the Real World to Understand a Glibc Bug | Lifting code to the specification level to study a complex concurrency bug. |
| Formal Specification for Authorization: Clarity Before Implementation | Applying TLA+ for better describing authorization requirements for systems. |
| Multi-Grained Specifications for Distributed System Model Checking and Verification | Review of multi-grained specifications combining high-level protocol models with fine-grained implementation details. |
| A Tale of Two Refinements | Generating Rust implementations from TLA+ specs using LLMs, building a concurrent system through stepwise refinement. |
| TLA+ in support of AI code generation | Using TLA+ specs as prompts for AI agent-mode code generation, demonstrating that the AI preserves specified algorithm correctness. |
| Verified Spec Transpilation with Claude | LLM-based verified transpilation from TLA+ specifications. |
| tla-specs | Collection of documented TLA+ explorations. |
Real-world specs (not part of TLA+ Examples)
| name | description | related resources |
|---|---|---|
| Linux kernel | TLA+ specs for kernel/arm64 work, including modeling qrwlock, qspinlock, and parts of arm64 | Formal Methods for Kernel Hackers (LPC 2018) · LPC 2018 slides (PDF) · LPC 2018 video · rs3lab/kernel-tla (rqspinlock) · A new type of spinlock for BPF (LWN) |
| glibc pthread_cond | TLA+ used for investigating and fixing the pthread condition-variable lost-wakeup bug | skarupke/glibc_tla_plus · Using TLA+ to Fix a Very Difficult glibc Bug (C++Now 2025 video) · glibc patch series |
| Elasticsearch Formal Models | TLA+ models of core Elasticsearch algorithms, including replication and replica engine behavior | Using TLA+ for fun and profit in the development of Elasticsearch (TLA+ Conf 2019) · Slides (PPTX) |
| etcd-io/raft | TLA+ spec and trace-validation work for the Raft algorithm as implemented by etcd | Runtime Protocol Refinement Checking for etcd-raft · Validating System Executions with the TLA+ Tools (TLA+ Conf 2024 slides) · Validating Traces of Distributed Programs Against TLA+ Specifications |
| TLA+ in TIDB | verify the distributed consensus algorithm : Raft & the implementation of distributed transaction. | |
| Servo web engine | TLA+ used to find and fix concurrency bugs in Servo's event-loop | Re-fixing Servo's event-loop (blog) · GOSIM China 2024 talk (video) · Slides (PDF) |
| Apache Kafka KRaft | TLA+ verification/spec work for KRaft features such as pre-vote and reconfiguration; TLA+ model also used to find bugs | Vanlightly/kafka-tlaplus · A Primer on Formal Verification and TLA+ · Detecting Bugs in Data Infrastructure using Formal Methods · Verifying Kafka Transactions diary · Distributed Systems Showdown: TLA+ vs Real Code (Hydra Conf slides) |
| Apache Kafka Replication | TLA+ specification of the Kafka ISR-based replication protocol, including KIP-101, KIP-279, and KIP-320; model checking revealed weaknesses in proposed designs | KIP-320 wiki (references TLA+ spec) |
| MongoDB Replication | TLA+ specs and trace-checking for MongoDB replication behavior/protocols | Fixing a MongoDB Replication Protocol Bug with TLA+ (TLA+ Conf 2019) · TLA+ Conf 2019 video · Rapid Prototyping a Logless Reconfiguration Protocol (MongoDB blog) · Modular Verification of MongoDB Transactions · Logless Dynamic Reconfiguration (paper) · eXtreme Modelling in Practice (paper) · eXtreme Modelling in Practice (video) |
| Signal SVR2 | TLA+ specification of the Raft-based consensus and self-healing protocol for Signal's Secure Value Recovery service, which stores PIN-protected secrets across multi-replica SGX enclaves | Secret Key Recovery in a Global-Scale End-to-End Encryption System (paper) |
| Xen vchan | TLA+ specification of the Xen vchan inter-domain communication protocol | Using TLA+ to Understand Xen Vchan (blog) |
| Ceph Consensus | TLA+ specification of the Ceph consensus algorithm (based on Paxos), derived from the actual Paxos.cc source code | Formal Verification of the Ceph Consensus Algorithm (thesis) · Formal Verification and Visualization (paper) |
| Raft Consensus Algorithm | TLA+ specification of the Raft consensus algorithm | |
| Raft Consensus Algorithm w/ Client | TLA+ specification of the Raft consensus algorithm and linearizable client | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) |
| Sequentially Consistent Raft Streams | TLA+ specification of an algorithm for sequentially consistent streaming responses from a Raft cluster | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) |
| tendermint-rs | Rust Tendermint implementation with TLA+ specifications | Verification Driven Development for Tendermint and IBC · How TLA+ and Apalache Helped Us Design the Tendermint Light Client (video) · A Tendermint Light Client (paper) |
| TendermintAcc | TLA+ specification of Tendermint consensus tuned for safety and fork accountability properties, including an inductive invariant | Verification Driven Development for Tendermint and IBC · Model-based Testing with TLA+ and Apalache (TLA+ Conf 2020 slides) |
| Tendermint Light Client | TLA+ specification of the Tendermint light client | How TLA+ and Apalache Helped Us Design the Tendermint Light Client (video) · Model-based Testing with TLA+ and Apalache (TLA+ Conf 2020 slides) · A Tendermint Light Client (paper) |
| celestia-tendermint-rs | Celestia fork of tendermint-rs, a Tendermint client framework with TLA+ specifications | |
| cometbft-rs | Rust CometBFT client framework with TLA+ specifications | |
| DualTor SONiC Protocol | TLA+ specification of the DualTor Standby/Active protocol for SONiC Top-of-Rack switches, verifying correctness of MUX failover and state machine coordination | |
| Apache BookKeeper | TLA+ specification of the BookKeeper replication protocol; found data-loss bugs in fencing and recovery | |
| EPaxos | TLA+ specs for the Egalitarian Paxos protocol, including EgalitarianPaxos.tla | EPaxos project page · EPaxos Revisited (NSDI'21) · On the Correctness of Egalitarian Paxos · Making Democracy Work: Fixing and Simplifying EPaxos (OPODIS'25) |
| SWIM Membership Protocol | TLA+ specification of the Scalable Weakly-consistent Infection-style Membership (SWIM) protocol | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) |
| Distributed Lock | TLA+ specification of a replicated state machine for distributed locking | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) · Distributed Systems in ONOS with Atomix 3 (ONF Connect 2018 slides) · ONF Connect 2018 video |
| Multi-primary Replication Protocol | TLA+ specification of a multi-primary replication protocol created for ONOS | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) · Distributed Systems in ONOS with Atomix 3 (ONF Connect 2018 slides) |
| P4Runtime Protocol Specification | TLA+ specification of the P4Runtime API that was used to demonstrate and fix safety violations in the protocol | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) |
| Flexible Paxos | TLA+ specification of Flexible Paxos, which revisits quorum intersection requirements in Paxos | Flexible Paxos paper · Flexible Paxos (the morning paper) · Dr TLA+ Series: Flexible Paxos (video) |
| Viewstamped Replication | TLA+ specifications of Viewstamped Replication; found a state transfer defect in the "VR Revisited" paper | VR Revisited analysis series (Jack Vanlightly) |
| CBC Casper | TLA+ and PlusCal specification of the CBC Casper consensus protocols (binary consensus) by Trail of Bits | Formal Analysis of the CBC Casper Consensus Algorithm with TLA+ (Trail of Bits blog) · CBC Casper paper |
| Event Driven HotStuff | PlusCal specification of the Event Driven HotStuff BFT consensus algorithm | discuss.tlapl.us thread · HotStuff: BFT Consensus in the Lens of Blockchain (paper) |
| TezEdge | TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus layers (Tezos blockchain) | |
| Succinct Atomic Swap | TLA+ specification of the Succinct Atomic Swap (SAS) Bitcoin smart contract protocol, verifying safety invariants and temporal properties | SAS protocol description (Ruben Somsen) · SAS presentation (video) · bitcoin-dev mailing list post |
| Katzenpost | TLA+ and Promela specifications of protocols for the Katzenpost mixnet anonymous communication network, including the directory authority voting protocol | discuss.tlapl.us thread |
| Generating All Combinations and Partitions | Spec of an algorithm in Knuth's TAOCP. It's Java implemenation is used by TLC. | |
| TaskScheduler | TLA+ specifications by Ubisoft validating lock-free MPSC/MCSP queue algorithms in a concurrent task scheduler, ensuring absence of deadlocks, reordering, and task loss | |
| lfest-rs | TLA+ specifications for a leveraged futures exchange simulator, verifying order execution and margin calculation logic | |
| Just-in-Time Paxos | TLA+ specification of an experimental consensus protocol that relies on high-precision clock synchronization to order proposals | |
| Spire Consensus | TLA+ specification and TLAPS machine-verifiable proof of the Spire single-value and Spanning Privilege (SP) multi-value consensus algorithms | Spire pre-print (TechRxiv) |
| zig-rcsp | TLA+ specification of a reference-counted shared pointer algorithm for Zig, verifying correctness of concurrent acquire/release operations |
TLA+ Video Resources
Most videos are hosted on the TLA+ Foundation YouTube channel.
Courses
Conference & Community Event Recordings
- TLA+ Community Event 2025
- TLA+ Conf 2024
- TLA+ Conf 2022
- TLA+ Conf 2021
- TLA+ Community Event 2020
- TLA+ Conf 2019
- TLA+ Community Meeting 2018
Topic Playlists
Standalone Talks
- Debugging software designs using testable pseudo-code (TLA+)
- The practice and Theory of TLA+
- Tackling Concurrency Bugs with TLA+
- Formal verification applied
- Thinking Above the Code
- Building confidence in concurrent code with a model checker (aka TLA+ for programmers)
Scientific papers
Theory
Tools
- Model Checking TLA+ Specifications
- Verifying Safety Properties with the TLA+ Proof System
- TLA+ model checking made symbolic
- The TLA+ Toolbox
Application
- eXtreme Modelling in Practice
- Specifying and Model Checking Workflows of Single Page Applications with TLA+
(University) courses teaching (with) TLA+
- York University: EECS4315 Mission-Critical Systems (Winter 2025 - Section Z)
- SUNY Buffalo: CSE 4/586 Distributed Systems (course page no longer available; Murat Demirbas's blog post on using TLA+ in teaching remains)
- Portland State: CS410/510 Practical Specification and Verification
- University of Wellington: SWEN421 - Formal Software Engineering
- Bordeaux INP: IF311 Formal Software Design
- RPTU Kaiserslautern-Landau: Programming Distributed Systems (formerly TU Kaiserslautern)
- University of Iowa: CS5620f15 Distributed Systems and Algorithms
- University of Tartu: Systems Modelling
- University of Colorado: Distributed Systems Verification
- University of California, San Diego: CSE 128 Spring 2005 Concurrency
- Loyola University Chicago: COMP 335/435 Formal Methods in Software Engineering (active, uses TLA+ alongside Java/jqwik)
- ISAE-SUPAERO: FITR304 Formal Verification and Validation (MSc, uses TLA+ alongside Frama-C/SPARK)
- Universidad Nacional de Rosario: Ingeniería de Software 1 (uses TLA+ and Z)
- Åbo Akademi University: Software Quality (MSc, uses TLA+ alongside Dafny/Rodin)
- TLA+ Foundation (formerly Microsoft Research): TLA+ Workshop EWD998 (currently not taught; teaching material available under a permissive license)
Contributors
Similar repos
README
Awesome TLA+
TLA+ is a formal specification and verification language to help engineers design, specify, reason about, and verify complex software and hardware systems. It is widely used to verify the algorithms in distributed systems.
Contents
- WebSites
- Discussions
- Users
- Tools
- Books
- TLA+ blog posts and articles
- Real-world specs
- TLA+ Video Resources
- Scientific papers
- (University) courses teaching (with) TLA+
WebSites
- Homepage: http://www.tlapl.us (https://lamport.azurewebsites.net/tla/tla.html)
- TLA+ Project: https://project.tlapl.us (https://github.com/tlaplus)
- TLA+ Community Modules: https://modules.tlapl.us/ (https://github.com/tlaplus/CommunityModules)
- TLA+ Examples: https://examples.tlapl.us (https://github.com/tlaplus/Examples)
- Learn TLA+ (PlusCal): https://learntla.com/
- Writing Specs: https://writingspecs.com/ — Beginner-friendly intro to writing specs and TLA+ concepts; WIP, not comprehensive.
Discussions
- google groups: https://groups.google.com/forum/#!forum/tlaplus
- reddit: https://www.reddit.com/r/tlaplus/
- twitter: https://twitter.com/tlaplus
- stackoverflow: https://stackoverflow.com/questions/tagged/tla%2b
Users
- Microsoft
- Atomix
- Informal Systems: TLA+ for protocol specification, model checking, model-based testing, and security audits of blockchains
- Open Networking Foundation
- Zilliqa Research
- TLA+ Foundation Industry page
Tools
Verification
- TLC: https://tools.tlapl.us (https://github.com/tlaplus/tlaplus)
- TLAPM: https://proofs.tlapl.us (https://github.com/tlaplus/tlapm)
- Apalache: https://apalache.informal.systems/
Experimental
IDEs
- VSCode-extension: https://github.com/tlaplus/vscode-tlaplus
- Toolbox (Eclipse based IDE): https://tools.tlapl.us (https://github.com/tlaplus/tlaplus) (no longer maintained)
- Jupyter notebook: https://github.com/kelvich/tlaplus_jupyter
- Emacs mode: https://github.com/ratish-punnoose/tla-mode
- Another Emacs mode: https://git.sdf.org/bch/tlamode/
- Intellij IDEA plugin: https://github.com/ocadaruma/tlaplus-intellij-plugin
- Web-based tool for exploring, visualizing, and sharing formal specs: https://github.com/will62794/spectacle
- Web-based learning platform: https://learning.tlapl.us
Misc
- Specula: https://github.com/specula-org/Specula/
- Better-comments (VSCode): https://github.com/alygin/better-comments
- TLC command-line wrapper: https://github.com/pmer/tla-bin
Parsers
- SANY (Syntactic Analyzer): A parser and syntax checker for TLA+ specifications
- TLAPS: A system for mechanically checking proofs written in TLA+
- tree-sitter-tlaplus: A tree-sitter grammar for TLA⁺ and PlusCal
- tlapy: A collection of Python tools for working with TLA+ specifications
Books
- Specifying Systems (freely available)
- Hyperbook (freely available)
- Practical TLA+
- TLA+ in Practice and Theory (freely available)
TLA+ blog posts and articles
| name | description |
|---|---|
| AWS and TLA+ | Use of Formal Methods at Amazon Web Services |
| Batch Installer | Sending async batches of commands. |
| Redux | Redux reducers with verifying a temporal property. |
| Zero Downtime Deployments | A simple model of a deploying new code to servers where at least one server is always available to clients, and all available servers show the same code version. |
| Trading Algorithm | Trading boths executing trades in a simulated market, showing how it’s susceptible to flash crashes. |
| Detecting Linked-List Cycles | Finding cycles in linked lists. |
| Replicated Storage | Replicated storage system with a quorum. |
| Rate Limiter | Independent workers hitting a rate-limited API. |
| Thread Pool | Multiple reader and writer threads sharing a bounded queue, discovering deadlocks. |
| Bank Transfer | Specifying a bank transfer with overdraft protection. |
| Finding bugs in systems through formalization | Ensuring distributed jobs go from “pending” to “completed”. |
| Building A "Simple" Distributed System | Rebalanser - distributed resource allocation library. |
| Train Sidings – A TLA+ Example | Railroad line where two trains can pass each other. |
| Azure Cosmos TLA+ specifications | The consistency levels offered by Azure Cosmos DB (also see Murat Demirbas' talk). |
| Modeling Streamlet in TLA+ | A PlusCal spec of a crash fault-tolerant variant of the Streamlet blockchain protocol. |
| Understanding Apache Hudi's Consistency Model | TLA+ specification and model checking of Hudi's consistency model |
| Using TLA+ in the Real World to Understand a Glibc Bug | Lifting code to the specification level to study a complex concurrency bug. |
| Formal Specification for Authorization: Clarity Before Implementation | Applying TLA+ for better describing authorization requirements for systems. |
| Multi-Grained Specifications for Distributed System Model Checking and Verification | Review of multi-grained specifications combining high-level protocol models with fine-grained implementation details. |
| A Tale of Two Refinements | Generating Rust implementations from TLA+ specs using LLMs, building a concurrent system through stepwise refinement. |
| TLA+ in support of AI code generation | Using TLA+ specs as prompts for AI agent-mode code generation, demonstrating that the AI preserves specified algorithm correctness. |
| Verified Spec Transpilation with Claude | LLM-based verified transpilation from TLA+ specifications. |
| tla-specs | Collection of documented TLA+ explorations. |
Real-world specs (not part of TLA+ Examples)
| name | description | related resources |
|---|---|---|
| Linux kernel | TLA+ specs for kernel/arm64 work, including modeling qrwlock, qspinlock, and parts of arm64 | Formal Methods for Kernel Hackers (LPC 2018) · LPC 2018 slides (PDF) · LPC 2018 video · rs3lab/kernel-tla (rqspinlock) · A new type of spinlock for BPF (LWN) |
| glibc pthread_cond | TLA+ used for investigating and fixing the pthread condition-variable lost-wakeup bug | skarupke/glibc_tla_plus · Using TLA+ to Fix a Very Difficult glibc Bug (C++Now 2025 video) · glibc patch series |
| Elasticsearch Formal Models | TLA+ models of core Elasticsearch algorithms, including replication and replica engine behavior | Using TLA+ for fun and profit in the development of Elasticsearch (TLA+ Conf 2019) · Slides (PPTX) |
| etcd-io/raft | TLA+ spec and trace-validation work for the Raft algorithm as implemented by etcd | Runtime Protocol Refinement Checking for etcd-raft · Validating System Executions with the TLA+ Tools (TLA+ Conf 2024 slides) · Validating Traces of Distributed Programs Against TLA+ Specifications |
| TLA+ in TIDB | verify the distributed consensus algorithm : Raft & the implementation of distributed transaction. | |
| Servo web engine | TLA+ used to find and fix concurrency bugs in Servo's event-loop | Re-fixing Servo's event-loop (blog) · GOSIM China 2024 talk (video) · Slides (PDF) |
| Apache Kafka KRaft | TLA+ verification/spec work for KRaft features such as pre-vote and reconfiguration; TLA+ model also used to find bugs | Vanlightly/kafka-tlaplus · A Primer on Formal Verification and TLA+ · Detecting Bugs in Data Infrastructure using Formal Methods · Verifying Kafka Transactions diary · Distributed Systems Showdown: TLA+ vs Real Code (Hydra Conf slides) |
| Apache Kafka Replication | TLA+ specification of the Kafka ISR-based replication protocol, including KIP-101, KIP-279, and KIP-320; model checking revealed weaknesses in proposed designs | KIP-320 wiki (references TLA+ spec) |
| MongoDB Replication | TLA+ specs and trace-checking for MongoDB replication behavior/protocols | Fixing a MongoDB Replication Protocol Bug with TLA+ (TLA+ Conf 2019) · TLA+ Conf 2019 video · Rapid Prototyping a Logless Reconfiguration Protocol (MongoDB blog) · Modular Verification of MongoDB Transactions · Logless Dynamic Reconfiguration (paper) · eXtreme Modelling in Practice (paper) · eXtreme Modelling in Practice (video) |
| Signal SVR2 | TLA+ specification of the Raft-based consensus and self-healing protocol for Signal's Secure Value Recovery service, which stores PIN-protected secrets across multi-replica SGX enclaves | Secret Key Recovery in a Global-Scale End-to-End Encryption System (paper) |
| Xen vchan | TLA+ specification of the Xen vchan inter-domain communication protocol | Using TLA+ to Understand Xen Vchan (blog) |
| Ceph Consensus | TLA+ specification of the Ceph consensus algorithm (based on Paxos), derived from the actual Paxos.cc source code | Formal Verification of the Ceph Consensus Algorithm (thesis) · Formal Verification and Visualization (paper) |
| Raft Consensus Algorithm | TLA+ specification of the Raft consensus algorithm | |
| Raft Consensus Algorithm w/ Client | TLA+ specification of the Raft consensus algorithm and linearizable client | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) |
| Sequentially Consistent Raft Streams | TLA+ specification of an algorithm for sequentially consistent streaming responses from a Raft cluster | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) |
| tendermint-rs | Rust Tendermint implementation with TLA+ specifications | Verification Driven Development for Tendermint and IBC · How TLA+ and Apalache Helped Us Design the Tendermint Light Client (video) · A Tendermint Light Client (paper) |
| TendermintAcc | TLA+ specification of Tendermint consensus tuned for safety and fork accountability properties, including an inductive invariant | Verification Driven Development for Tendermint and IBC · Model-based Testing with TLA+ and Apalache (TLA+ Conf 2020 slides) |
| Tendermint Light Client | TLA+ specification of the Tendermint light client | How TLA+ and Apalache Helped Us Design the Tendermint Light Client (video) · Model-based Testing with TLA+ and Apalache (TLA+ Conf 2020 slides) · A Tendermint Light Client (paper) |
| celestia-tendermint-rs | Celestia fork of tendermint-rs, a Tendermint client framework with TLA+ specifications | |
| cometbft-rs | Rust CometBFT client framework with TLA+ specifications | |
| DualTor SONiC Protocol | TLA+ specification of the DualTor Standby/Active protocol for SONiC Top-of-Rack switches, verifying correctness of MUX failover and state machine coordination | |
| Apache BookKeeper | TLA+ specification of the BookKeeper replication protocol; found data-loss bugs in fencing and recovery | |
| EPaxos | TLA+ specs for the Egalitarian Paxos protocol, including EgalitarianPaxos.tla | EPaxos project page · EPaxos Revisited (NSDI'21) · On the Correctness of Egalitarian Paxos · Making Democracy Work: Fixing and Simplifying EPaxos (OPODIS'25) |
| SWIM Membership Protocol | TLA+ specification of the Scalable Weakly-consistent Infection-style Membership (SWIM) protocol | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) |
| Distributed Lock | TLA+ specification of a replicated state machine for distributed locking | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) · Distributed Systems in ONOS with Atomix 3 (ONF Connect 2018 slides) · ONF Connect 2018 video |
| Multi-primary Replication Protocol | TLA+ specification of a multi-primary replication protocol created for ONOS | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) · Distributed Systems in ONOS with Atomix 3 (ONF Connect 2018 slides) |
| P4Runtime Protocol Specification | TLA+ specification of the P4Runtime API that was used to demonstrate and fix safety violations in the protocol | Bridging the Verifiability Gap (TLA+ Conf 2020 slides) |
| Flexible Paxos | TLA+ specification of Flexible Paxos, which revisits quorum intersection requirements in Paxos | Flexible Paxos paper · Flexible Paxos (the morning paper) · Dr TLA+ Series: Flexible Paxos (video) |
| Viewstamped Replication | TLA+ specifications of Viewstamped Replication; found a state transfer defect in the "VR Revisited" paper | VR Revisited analysis series (Jack Vanlightly) |
| CBC Casper | TLA+ and PlusCal specification of the CBC Casper consensus protocols (binary consensus) by Trail of Bits | Formal Analysis of the CBC Casper Consensus Algorithm with TLA+ (Trail of Bits blog) · CBC Casper paper |
| Event Driven HotStuff | PlusCal specification of the Event Driven HotStuff BFT consensus algorithm | discuss.tlapl.us thread · HotStuff: BFT Consensus in the Lens of Blockchain (paper) |
| TezEdge | TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus layers (Tezos blockchain) | |
| Succinct Atomic Swap | TLA+ specification of the Succinct Atomic Swap (SAS) Bitcoin smart contract protocol, verifying safety invariants and temporal properties | SAS protocol description (Ruben Somsen) · SAS presentation (video) · bitcoin-dev mailing list post |
| Katzenpost | TLA+ and Promela specifications of protocols for the Katzenpost mixnet anonymous communication network, including the directory authority voting protocol | discuss.tlapl.us thread |
| Generating All Combinations and Partitions | Spec of an algorithm in Knuth's TAOCP. It's Java implemenation is used by TLC. | |
| TaskScheduler | TLA+ specifications by Ubisoft validating lock-free MPSC/MCSP queue algorithms in a concurrent task scheduler, ensuring absence of deadlocks, reordering, and task loss | |
| lfest-rs | TLA+ specifications for a leveraged futures exchange simulator, verifying order execution and margin calculation logic | |
| Just-in-Time Paxos | TLA+ specification of an experimental consensus protocol that relies on high-precision clock synchronization to order proposals | |
| Spire Consensus | TLA+ specification and TLAPS machine-verifiable proof of the Spire single-value and Spanning Privilege (SP) multi-value consensus algorithms | Spire pre-print (TechRxiv) |
| zig-rcsp | TLA+ specification of a reference-counted shared pointer algorithm for Zig, verifying correctness of concurrent acquire/release operations |
TLA+ Video Resources
Most videos are hosted on the TLA+ Foundation YouTube channel.
Courses
Conference & Community Event Recordings
- TLA+ Community Event 2025
- TLA+ Conf 2024
- TLA+ Conf 2022
- TLA+ Conf 2021
- TLA+ Community Event 2020
- TLA+ Conf 2019
- TLA+ Community Meeting 2018
Topic Playlists
Standalone Talks
- Debugging software designs using testable pseudo-code (TLA+)
- The practice and Theory of TLA+
- Tackling Concurrency Bugs with TLA+
- Formal verification applied
- Thinking Above the Code
- Building confidence in concurrent code with a model checker (aka TLA+ for programmers)
Scientific papers
Theory
Tools
- Model Checking TLA+ Specifications
- Verifying Safety Properties with the TLA+ Proof System
- TLA+ model checking made symbolic
- The TLA+ Toolbox
Application
- eXtreme Modelling in Practice
- Specifying and Model Checking Workflows of Single Page Applications with TLA+
(University) courses teaching (with) TLA+
- York University: EECS4315 Mission-Critical Systems (Winter 2025 - Section Z)
- SUNY Buffalo: CSE 4/586 Distributed Systems (course page no longer available; Murat Demirbas's blog post on using TLA+ in teaching remains)
- Portland State: CS410/510 Practical Specification and Verification
- University of Wellington: SWEN421 - Formal Software Engineering
- Bordeaux INP: IF311 Formal Software Design
- RPTU Kaiserslautern-Landau: Programming Distributed Systems (formerly TU Kaiserslautern)
- University of Iowa: CS5620f15 Distributed Systems and Algorithms
- University of Tartu: Systems Modelling
- University of Colorado: Distributed Systems Verification
- University of California, San Diego: CSE 128 Spring 2005 Concurrency
- Loyola University Chicago: COMP 335/435 Formal Methods in Software Engineering (active, uses TLA+ alongside Java/jqwik)
- ISAE-SUPAERO: FITR304 Formal Verification and Validation (MSc, uses TLA+ alongside Frama-C/SPARK)
- Universidad Nacional de Rosario: Ingeniería de Software 1 (uses TLA+ and Z)
- Åbo Akademi University: Software Quality (MSc, uses TLA+ alongside Dafny/Rodin)
- TLA+ Foundation (formerly Microsoft Research): TLA+ Workshop EWD998 (currently not taught; teaching material available under a permissive license)