Skip to content

kaelzhang81/awesome-tlaplus

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

8 Commits
 
 
 
 

Repository files navigation

awesome-tlaplus

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.

WebSite

blogs

TLA+ Cases

name description
AWS and TLA+ Use of Formal Methods at Amazon Web Services
Batch Installer (H) Sending async batches of commands.
Redux (H) Redux reducers with verifying a temporal property.
Zero Downtime Deployments (H) 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 (H) Independent workers hitting a rate-limited API.
Thread Pool (T) Multiple reader and writer threads sharing a bounded queue, discovering deadlocks.
Bank Transfer (H) Specifying a bank transfer with overdraft protection.
Finding bugs in systems through formalization Ensuring distributed jobs go from “pending” to “completed”.
TLA+ in TIDB verify the distributed consensus algorithm : Raft & the implementation of distributed transaction.

TLA+ Video Resources

TLA+ Example

  • allocator

    Specification of a resource allocator, written by Stephan Merz.

  • CarTalkPuzzle

    A TLA+ specification of the solution to a nice puzzle.

  • chang_roberts

    A PlusCal specification of the algorithm by Chang and Roberts (1979) for electing a leader on a unidirectional ring.

  • DieHard

    A very elementary example based on a puzzle from a movie. It provides a good first introduction to TLA+.

  • dijkstra-mutex

    A PlusCal version of the first published mutual exclusion algorithm, written by Edsger Dijkstra.

  • ewd840 A TLA+ specification of an algorithm due to Dijkstra, Feijen, and van Gasteren for detecting distributed termination on a unidirectional ring, together with a safety proof.

  • lamport_mutex A TLA+ specification of the distributed mutual-exclusion algorithm that appeared as an example in Lamport's classic paper "Time, Clocks and the Ordering of Events in a Distributed System", together with a hierarchical proof of mutual exclusion.

  • N-Queens TLA+ and PlusCal descriptions of a solution to the N queens problem. Written by Stephan Merz.

  • Paxos

    A high-level specification of the Paxos consensus algorithm, consisting of a specification of consensus, a very high level spec of the algorithm (with no messages) that implements consensus and is implemented by the Paxos algorithm.

  • Prisoners

    A simple specification that solves a puzzle that was presented on an American radio program. The solution is rather subtle, and hence it's not so easy to understand why the solution is correct.

  • Specifying Systems Examples to accompany the book Specifying Systems.

  • Stones

    Another specification that solves the same proble as CarTalkPuzzle.

  • sums_even

    Two proofs for showing that x+x is even, for any natural number x.

  • tower_of_hanoi

    The well-known Towers of Hanoi puzzle.

  • transaction_commit

    TLA+ specifications underlying the paper "Consensus on Transaction Commit" by Gray and Lamport (2006).

  • TransitiveClosure

    Someone once posted on TLAPlus.net a question asking how the transitive closure of a relation can be defined in TLA+. This answers the question by giving several equivalent definitions. Reading them might help you when you have to define some mathematical operation that requires a recursive definition.

  • TwoPhase

    A specification of a very simple hardware protocol and of the problem it solves. This is a nice example of the use of instantiation to describe a refinement mapping, and of the use of constant operator parameters to describe unspecified actions. There is also a TLA+ proof of correctness that has been checked by the TLAPS proof system.

enjoy it! 😄

About

A curated list of TLA+ resources.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published