A collection of TLA⁺ specifications of varying complexities

Dr. TLA+ series - learn an algorithm and protocol, study a specification

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

PGo is a source to source compiler from Modular PlusCal specs into Go programs.

TLA+ specifications accompanying paper: Automated Validation of State-Based Client-Centric Isolation with TLA+. (https://doi.org/10.1007/978-3-030-67220-1_4) Based on Crooks' Isolation (https://dl.acm.org/doi/10.1145/3087801.3087802).

How to use TLA+ / TLA+ specification of the ClickHouse replication protocol

TLA+ programs

A TLA+ verification of the Go-Back-N ARQ protocol

Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.

Utilities for TLA+ and PlusCal

Formal verification of UML state machines with Promela and TLA+/PlusCal

Collection of useful "operators" (functions) to make TLA+ easier to learn and to use

Implementation and validation of the model checking of various Distributed System algorithms like BenOr, Paxos, etc. using PlusCal and TLA+, also analyze the temporal and invariant properties.

Learning and experimenting with TLA toy models

Experimenting with formal methods using TLA+ and Pluscal

Bully election algorithm model written in TLA+ and PlusCal

Go-Back-N specified in TLA+/ PlusCal

Modelling the Zcash P2P network