TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

Distributed Systems Labs and Framework

A collection of TLA⁺ specifications of varying complexities.

Hermit launches linux x86_64 programs in a special, hermetically isolated sandbox to control their execution. Hermit translates normal, nondeterministic behavior, into deterministic, repeatable beh…

Add hardship to your tests

Rust implementation of stack graphs

APALACHE: symbolic model checker for TLA+ and Quint

TLA+ language support for Visual Studio Code

Interactive playground for exploring and sharing TLA+ specifications in the browser.

The main development version of the PRISM model checker.

A user-ready linux image/rootfs for the Pine64 Pinenote based on Debian trixie and GNOME

The TLA⁺ Proof Manager

Eco CI Energy estimation for Github Actions, GitLab and Jenkins

Patches include sunxi platform support and various driver fixes

Replicated State Library. RSL is the Azure Paxos implementation which is used by multiple products in Azure and Bing. It provides the traditional Paxos functionality in a real world implementation.…

A tree-sitter grammar for TLA⁺ and PlusCal

A framework for distributed applications

Reading the linearizability paper with TLA+

In Spec We Trust

Rewrites TLA⁺ specs to use Unicode symbols instead of ASCII, and vice-versa

Experimental tree-sitter parser for the Lean (4) Theorem Prover

TLA+/PlusCal support for Neovim

TLA+ Foundation

Basic TLA+ related Haskell libraries (parser, evaluator, pretty-printer)

Tutorial on modeling with TLA+

Tool for automatically inferring inductive invariants of distributed protocols.

Some experiments in making exercises for teaching TLA+

Human-like theorem prover, inspired by robotone and developed in the Coq ecosystem.

A formatter for TLA+ specs