awesome-tlaplus
awesome-tlaplus copied to clipboard
Published
20 hours ago •
tlaplus
tlaplus
A curated list of TLA+ resources.
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/
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
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/
IDEs
- 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
Misc
- 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. |
| 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. |
TLA+ Video Resources
- 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)
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+
- 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
tlaplus