tlaplus

A collection of TLA+ specifications of varying complexities

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

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!

A gently curated list of companies using verification formal methods in industry

APALACHE: symbolic model checker for TLA+

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

A static web application to explore and animate a TLA+ state graph.

A script for running TLA+/TLC from the command line

Quint is an executable specification language with design and tooling focused on usability. It is based on the Temporal Logic of Actions

Advanced fuzzing via Model Based Testing for Cosmos blockchains

A tree-sitter grammar for TLA⁺ and PlusCal

Model-based testing tool

Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF

Distributed termination detection on a ring, due to Shmuel Safra:

A TLA+ module for animating TLC traces.

Proving a blocking queue deadlock free in a dozen different ways

Specifying and Verifying CRDT Protocols using TLA+

Reading the linearizability paper with TLA+

🔬 formal tools for BPMN

Different TLA+ specifications, mostly for learning purposes