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.
- WebSites
- Discussions
- Users
- Tools
- Books
- TLA+ blog posts and articles
- Real-world specs
- TLA+ Video Resources
- Scientific papers
- (University) courses teaching (with) TLA+
- 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.
- 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
- 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
- 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/
- 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
- 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
- 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
- Specifying Systems (freely available)
- Hyperbook (freely available)
- Practical TLA+
- TLA+ in Practice and Theory (freely available)
| 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 |
Most videos are hosted on the TLA+ Foundation YouTube channel.
- TLA+ Community Event 2025
- TLA+ Conf 2024
- TLA+ Conf 2022
- TLA+ Conf 2021
- TLA+ Community Event 2020
- TLA+ Conf 2019
- TLA+ Community Meeting 2018
- 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)
- Model Checking TLA+ Specifications
- Verifying Safety Properties with the TLA+ Proof System
- TLA+ model checking made symbolic
- The TLA+ Toolbox
- eXtreme Modelling in Practice
- Specifying and Model Checking Workflows of Single Page Applications 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)