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/
- 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
- 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)
- 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
- 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. |
| Using TLA+ in the Real World to Understand a Glibc Bug | Lifting code to the specification level to study a complex concurrency bug. |
| tla-specs | Collection of documented TLA+ explorations. |
Real-world specs (not part of TLA+ Examples)
| name | description |
|---|---|
| Distributed Lock | TLA+ specification of a replicated state machine for distributed locking |
| Generating All Combinations and Partitions | Spec of an algorithm in Knuth's TAOCP. It's Java implemenation is used by TLC. |
| Just-in-Time Paxos | TLA+ specification of an experimental consensus protocol that relies on high-precision clock synchronization to order proposals |
| Multi-primary Replication Protocol | TLA+ specification of a multi-primary replication protocol created for ONOS |
| P4Runtime Protocol Specification | TLA+ specification of the P4Runtime API that was used to demonstrate and fix safety violations in the protocol |
| 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 |
| Sequentially Consistent Raft Streams | TLA+ specification of an algorithm for sequentially consistent streaming responses from a Raft cluster |
| SWIM Membership Protocol | TLA+ specification of the Scalable Weakly-consistent Infection-style Membership (SWIM) protocol |
| TendermintAcc | TLA+ specification of Tendermint consensus tuned for safety and fork accountability properties, including an inductive invariant |
| Tendermint Light Client | TLA+ specification of the Tendermint light client |
| TLA+ in TIDB | verify the distributed consensus algorithm : Raft & the implementation of distributed transaction. |
- The TLA+ Video Course
- Dr TLA+
- TLA+ Community Meeting 2018
- TLA+ conf 2019
- 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+
- EECS4315 Mission-Critical Systems (Winter 2023 - Section Z)
- SUNY Buffalo: CSE 4/586 Distributed Systems (Notes)
- Portland State: CS410/510 Practical Specification and Verification
- University of Wellington: SWEN421 - Formal Software Engineering
- Bordeaux INP: IF311 Formal Software Design
- TU Kaiserslautern: Programming Distributed Systems
- 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