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

A tree-sitter grammar for TLA⁺ and PlusCal

Tool for automatically inferring inductive invariants of distributed protocols.

A collection of various standards, proposed or established, related to TLA+

Verification tool for distributed protocols based on inductive proof decomposition.

This tool synthesizes symbolic assumptions for TLA+ specifications.

High level model for MongoDB consistency

TLAi+ Benchmarks

Synchronous fault-tolerant distributed algorithms encoded in TLA+

Artifact for the VLDB 2025 paper, "Design and Modular Verification of Distributed Transactions in MongoDB". Includes TLA+ specifications and code for model-based testing of the WiredTiger API.