A collection of TLA⁺ specifications of varying complexities.

• UpdatedMar 7, 2025
• TLA

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

• UpdatedMar 18, 2025
• TypeScript

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

• UpdatedApr 18, 2022
• TLA

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

• UpdatedFeb 11, 2025

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

• UpdatedOct 27, 2024
• TLA

APALACHE: symbolic model checker for TLA+ and Quint

• UpdatedJan 22, 2025
• Scala

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

• UpdatedMar 15, 2025
• TLA

Learn TLA+ for free! No prior experience necessary!

• UpdatedMar 17, 2025
• TLA

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

• UpdatedNov 8, 2023
• JavaScript

Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

• UpdatedMar 17, 2025
• Python

Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+.

• UpdatedMar 18, 2025
• JavaScript

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

• UpdatedApr 20, 2021
• Python

Advanced fuzzing via Model Based Testing for Cosmos blockchains

• UpdatedApr 6, 2023
• Python

A selection of textbook-like course notes for the Imperial College Computing modules.

• UpdatedMar 23, 2024
• TeX

Generate (message) sequence diagrams from TLA+ state traces

• UpdatedFeb 5, 2023
• Python

A tree-sitter grammar for TLA⁺ and PlusCal

• UpdatedFeb 26, 2025
• C

Model-based testing tool

• UpdatedMar 12, 2025
• Python

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

• UpdatedSep 2, 2024
• TLA

Reading the linearizability paper with TLA+

• UpdatedApr 24, 2022
• TLA

A TLA+ module for animating TLC traces.

• UpdatedDec 9, 2024
• TLA