Skip to content

SYSTEM Cited by 3 sources

TLA+

Overview

TLA+ is Leslie Lamport's specification language for describing concurrent + distributed systems. A TLA+ spec describes an algorithm as a state machine: a set of state variables, an initial state, and a set of allowed transitions. Safety and liveness properties are stated as temporal-logic invariants over behaviours (paths through the state graph).

TLA+'s tooling ecosystem — especially the TLC model-checker — lets engineers mechanically verify their specs satisfy stated properties, and (with more work) conformance-check that production implementations behave as the spec says.

Concrete use at MongoDB

MongoDB's server team has a long practice of writing TLA+ specs of its own consensus and replication protocols. Public specs live in the MongoDB mongo tla_plus directory. The canonical wiki instance is RaftMongo.tla — the spec of how servers learn the commit point in MongoDB's Raft-like consensus protocol.

Other specs (named in Davis 2025; not catalogued individually here): replication, transactions, WiredTiger storage layer (the last is the basis of VLDB 2025's Design and Modular Verification of Distributed Transactions in MongoDB).

Why it comes up in conformance checking

TLA+ is the default "formal spec language" for production distributed systems. A spec model-checks → the algorithm is correct as specified. The open question is whether the production implementation actually behaves that way. That's conformance checking:

  • patterns/trace-checking — translate impl execution traces into TLA+ (typically via Ron Pressler's technique); ask TLC whether each trace is a valid behaviour of the spec.
  • patterns/test-case-generation-from-spec — enumerate behaviours of the spec using TLC; emit one unit test per behaviour that forces the impl to follow it.

Both require the impl to exist and the spec to exist and the mapping between them to be maintainable. The MongoDB 2020 experiment (Source: sources/2025-06-02-mongodb-conformance-checking-at-mongodb-testing-that-our-code-matches-our-tla-specs) failed at trace-checking (spec + impl written years apart at mismatched abstraction) and succeeded at test-case generation (Mobile SDK's OT merge rules).

Operational notes

  • Companion checker: TLC is the primary finite-state checker. Recent features (2024) support incomplete trace inference — log only some state variables and let TLC fill in the rest — which reduces the atomic-state-snapshot burden for trace-checking.
  • PlusCal / +CAL — an imperative-style front-end that compiles to TLA+. Used in some of the successor academic systems (Choreographic PlusCal for Go trace-logging).
  • TLA+-to-Go — Finn Hackett's compiler generates Go code from TLA+ specs. Target: narrow the spec-to-impl gap by making the two literally the same artifact.

Ecosystem adoption

  • AWS — uses TLA+ since 2014 (S3, DynamoDB, EBS). TLA+ specs are used up-front at design time; conformance checking on the implementation is not the primary stance (lightweight formal verification with in-language executable specs is). Byron Cook's sources/2026-02-17-allthingsdistributed-byron-cook-automated-reasoning-trust-ai|2026-02 framing positions TLA+ as one tool in a broader automated-reasoning toolkit, not the central one.
  • MongoDB — uses TLA+ for consensus + replication + transactions + storage-layer specs. Actively researching conformance checking (VLDB 2020, VLDB 2025, ongoing Antithesis + Finn Hackett collaborations).
  • Microsoft Azure — used TLA+ for Cosmos DB and other services.
  • Academic research — Mocket, SandTable, Multi-Grained Zookeeper, Confidential Consortium Framework conformance experiments all built on TLA+.

Seen in

Last updated · 200 distilled / 1,178 read