Skip to content

tlaplus/awesome-tlaplus

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

40 Commits
 
 
 
 
 
 

Repository files navigation

Awesome TLA+ Awesome

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

Verification

IDEs

Misc

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

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

Scientific papers

Theory

Tools

Application

(University) courses teaching (with) TLA+

About

A curated list of TLA+ resources.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published