TLA+ Formal Verification for Distributed Protocols

Overview

Distributed systems fail in ways that unit tests and integration tests rarely surface. A transaction coordinator can crash between writing a prepare record and sending ACKs. A shard split can interleave with an in-flight read in a way that exposes inconsistent data for exactly one linearizability window. A snapshot transfer can stall mid-stream while the source continues accepting writes. These bugs are not hypothetical—they are the class of defect that takes down production systems and is nearly impossible to reproduce reliably. TLA+ is the industrial-strength tool for finding them before they ship.

TLA+ (Temporal Logic of Actions) is a formal specification language created by Leslie Lamport. It describes a system as a state machine: an initial state predicate, a next-state relation that defines all legal transitions, and temporal properties (invariants, liveness conditions) that must hold across every possible execution. The TLA+ model checker, TLC, exhaustively explores every reachable state of a specification and reports any execution that violates a declared property. For a protocol like two-phase commit over sharded storage, TLC will find the exact sequence of steps—including concurrent operations on different nodes and arbitrary message reorderings—that leads to a consistency violation.

A well-maintained distributed system can accumulate tens of thousands of lines of TLA+ specifications covering transactions, shard splits, and snapshot transfers. These specs are not documentation artifacts; they are active model-checked artifacts that catch real bugs during development. The accompanying runtime trace validator translates production execution logs into TLA+ traces and checks them against the specification, bridging the gap between the abstract model and the concrete implementation. This document explains how to write, structure, and leverage TLA+ specifications at this scale.

Core Concepts

How It Works

A production-grade TLA+ methodology is typically structured in three tiers: abstract protocol specifications, concrete implementation specifications with failure models, and runtime trace validators that link logs to specs. Each tier has a distinct purpose and a distinct audience.

Abstract Protocol Specification: Two-Phase Commit

The abstract specification captures the essential safety and liveness properties of a protocol without implementation details. For two-phase commit across shards, the key safety property is that no two participants can reach conflicting decisions (one commits, one aborts) for the same transaction. The following is representative of the style used in the readiness-report specs:

---- MODULE TwoPhaseCommit ----
EXTENDS Naturals, FiniteSets, TLC

CONSTANTS RM          \* set of resource managers (shards)

VARIABLES
    rmState,          \* rmState[r] \in {"working", "prepared", "committed", "aborted"}
    tmState,          \* tmState \in {"init", "committed", "aborted"}
    tmPrepared        \* set of RMs that have sent Prepare to TM

TypeOK ==
    /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
    /\ tmState \in {"init", "committed", "aborted"}
    /\ tmPrepared \subseteq RM

Init ==
    /\ rmState = [r \in RM |-> "working"]
    /\ tmState = "init"
    /\ tmPrepared = {}

\* Resource manager sends Prepare
RMPrepare(r) ==
    /\ rmState[r] = "working"
    /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
    /\ tmPrepared' = tmPrepared \cup {r}
    /\ UNCHANGED tmState

\* Transaction manager commits once all RMs prepared
TMCommit ==
    /\ tmState = "init"
    /\ tmPrepared = RM
    /\ tmState' = "committed"
    /\ rmState' = [r \in RM |-> "committed"]
    /\ UNCHANGED tmPrepared

\* Transaction manager aborts (any time before commit)
TMAbort ==
    /\ tmState = "init"
    /\ tmState' = "aborted"
    /\ rmState' = [r \in RM |-> "aborted"]
    /\ UNCHANGED tmPrepared

Next ==
    \/ TMCommit
    \/ TMAbort
    \/ \E r \in RM : RMPrepare(r)

\* Safety: no two RMs can have conflicting decisions
Consistent ==
    \A r1, r2 \in RM :
        ~ /\ rmState[r1] = "aborted"
          /\ rmState[r2] = "committed"

Spec == Init /\ [][Next]_<<rmState, tmState, tmPrepared>>

THEOREM Spec => [](TypeOK /\ Consistent)
====

Concrete Specification with Message Passing and Failures

The concrete specification adds network messages, coordinator crash-recovery, and the WAL write ordering that the implementation must follow. Message delivery is modeled as a set of in-flight messages; any enabled action can receive any message currently in the network. Crash-recovery is modeled as a Crash(r) action that resets the node’s volatile state while preserving its durable state, and a Recover(r) action that reconstructs in-memory state from the WAL:

---- MODULE TwoPhaseCommitMsg ----
EXTENDS Naturals, FiniteSets, Sequences, TLC

CONSTANTS RM

VARIABLES
    rmState,
    tmState,
    tmPrepared,
    msgs,             \* set of in-flight messages
    rmLog,            \* rmLog[r] = sequence of WAL records (durable)
    tmLog             \* tmLog = sequence of WAL records (durable)

\* TM crashes: loses in-memory state, keeps durable log
TMCrash ==
    /\ tmState' = "init"
    /\ tmPrepared' = {}
    /\ UNCHANGED <<rmState, msgs, rmLog, tmLog>>

\* TM recovers: reconstructs state from durable log
TMRecover ==
    /\ tmState = "init"
    /\ LET lastDecision == LastDecisionInLog(tmLog)
       IN tmState' = IF lastDecision = "none" THEN "init"
                     ELSE lastDecision
    /\ UNCHANGED <<rmState, tmPrepared, msgs, rmLog, tmLog>>

\* RM receives abort message after a crash (idempotent)
RMRcvAbortMsg(r) ==
    /\ [type |-> "Abort"] \in msgs
    /\ rmState[r] \notin {"aborted"}
    /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
    /\ rmLog' = [rmLog EXCEPT ![r] = Append(rmLog[r], "aborted")]
    /\ UNCHANGED <<tmState, tmPrepared, msgs, tmLog>>

====

Shard Split Specification

Shard splits are particularly subtle because they require the splitting shard to stop accepting writes for the affected key range, transfer data to the new shard, and then atomically update the routing table—all while in-flight reads and writes may be targeting the splitting range. The TLA+ spec captures this with explicit “splitting” and “frozen” states for shards:

---- MODULE ShardSplit ----
EXTENDS Naturals, FiniteSets, TLC

CONSTANTS Keys, Shards

VARIABLES
    shardState,       \* shardState[s] \in {"active", "splitting", "frozen", "retired"}
    shardRange,       \* shardRange[s] = set of keys owned by shard s
    routing,          \* routing[k] = shard currently owning key k
    pendingWrites     \* writes in flight before freeze

\* No key can be owned by two active shards simultaneously
SingleOwner ==
    \A k \in Keys :
        Cardinality({s \in Shards :
            /\ routing[k] = s
            /\ shardState[s] \in {"active", "splitting"}}) = 1

\* All in-flight writes before freeze must complete before retirement
SafeRetire(s) ==
    /\ shardState[s] = "frozen"
    /\ pendingWrites[s] = {}
    /\ shardState' = [shardState EXCEPT ![s] = "retired"]
    /\ UNCHANGED <<shardRange, routing, pendingWrites>>

====

Runtime Trace Validator

The runtime validator is a Go program that reads structured log lines from the production system and reconstructs a TLA+ state sequence. It then feeds this sequence to TLC in “simulation mode” and checks whether each step is a valid Next transition:

package tlavalidator

import (
    "bufio"
    "encoding/json"
    "fmt"
    "io"
    "os"
    "os/exec"
)

// TraceEntry is one structured log line from the production system.
type TraceEntry struct {
    Timestamp int64             `json:"ts"`
    Action    string            `json:"action"`   // e.g. "RMPrepare", "TMCommit"
    Vars      map[string]any    `json:"vars"`     // current variable values after action
}

// ValidateTrace replays a log file against the TLA+ specification.
// It invokes TLC with the -simulate flag and feeds the trace as an override.
func ValidateTrace(specPath, logPath string) error {
    entries, err := loadTrace(logPath)
    if err != nil {
        return fmt.Errorf("load trace: %w", err)
    }

    overridePath, err := writeTraceOverride(entries)
    if err != nil {
        return fmt.Errorf("write override: %w", err)
    }
    defer os.Remove(overridePath)

    cmd := exec.Command("java", "-jar", "tla2tools.jar",
        "-simulate", "-traceFile", overridePath, specPath)
    cmd.Stdout = os.Stdout
    cmd.Stderr = os.Stderr
    if err := cmd.Run(); err != nil {
        return fmt.Errorf("TLC violation found: %w", err)
    }
    return nil
}

func loadTrace(path string) ([]TraceEntry, error) {
    f, err := os.Open(path)
    if err != nil {
        return nil, err
    }
    defer f.Close()

    var entries []TraceEntry
    scanner := bufio.NewScanner(f)
    for scanner.Scan() {
        var e TraceEntry
        if err := json.Unmarshal(scanner.Bytes(), &e); err != nil {
            return nil, fmt.Errorf("parse log line: %w", err)
        }
        entries = append(entries, e)
    }
    return entries, scanner.Err()
}

func writeTraceOverride(entries []TraceEntry) (string, error) {
    f, err := os.CreateTemp("", "tla-trace-*.json")
    if err != nil {
        return "", err
    }
    defer f.Close()
    enc := json.NewEncoder(f)
    for _, e := range entries {
        if err := enc.Encode(e); err != nil {
            return "", err
        }
    }
    return f.Name(), nil
}

Instrumentation: Emitting Structured Trace Logs

For the trace validator to work, the Go implementation must emit one structured log entry per state transition, including the complete post-transition variable state. A lightweight trace logger wraps the critical protocol actions:

package tlatrace

import (
    "encoding/json"
    "log/slog"
    "time"
)

// Logger emits TLA+-compatible trace entries to a structured logger.
type Logger struct {
    log *slog.Logger
}

func New(l *slog.Logger) *Logger { return &Logger{log: l} }

// Emit records a single TLA+ action with the post-action variable snapshot.
func (tl *Logger) Emit(action string, vars map[string]any) {
    entry := map[string]any{
        "ts":     time.Now().UnixMilli(),
        "action": action,
        "vars":   vars,
    }
    raw, _ := json.Marshal(entry)
    tl.log.Info("tla_trace", "entry", string(raw))
}

// Example usage inside the transaction coordinator:
//
//   tl.Emit("TMCommit", map[string]any{
//       "tmState":    "committed",
//       "tmPrepared": preparedSet,
//       "rmState":    rmStateMap,
//   })

Implementation Patterns

Structuring a Large Specification (86K+ Lines)

At scale (86,000+ lines of TLA+), specifications are organized as a module hierarchy. The top-level modules import reusable sub-modules for common patterns:

---- MODULE TransactionProtocol ----
\* Top-level spec that instantiates sub-modules

EXTENDS Integers, FiniteSets, Sequences, TLC

\* Import shared utilities
INSTANCE MessagePassing WITH
    MaxMessages <- MAX_INFLIGHT_MSGS

\* Import the shard split sub-spec
ShardSplitSpec == INSTANCE ShardSplit WITH
    Keys  <- ALL_KEYS,
    Shards <- ALL_SHARDS

\* Import the snapshot transfer sub-spec
SnapshotSpec == INSTANCE SnapshotTransfer WITH
    Nodes <- SHARD_NODES

====

Parameterized Model Constants for TLC

TLC requires concrete finite values for all CONSTANTS. The model configuration file sets small but representative values that keep the state space tractable while exercising the key interleavings:

\* TwoPhaseCommit.cfg (TLC model configuration)
CONSTANTS
    RM = {r1, r2, r3}       \* 3 resource managers
    Keys = {k1, k2, k3}     \* 3 keys
    Shards = {s1, s2}       \* 2 shards (one split produces a third)
    MAX_INFLIGHT_MSGS = 4   \* bound message queue depth

SYMMETRY Permutations(RM)   \* treat all RMs as interchangeable

INVARIANTS
    TypeOK
    Consistent
    SingleOwner

PROPERTIES
    \* Every prepared transaction eventually commits or aborts
    [](\A r \in RM : rmState[r] = "prepared" => <>(rmState[r] \in {"committed", "aborted"}))

CHECK_DEADLOCK TRUE

Snapshot Transfer Specification

Snapshot transfers must ensure that every key present at the start of the transfer is present in the snapshot, and that writes arriving during the transfer are captured exactly once—either in the snapshot or in the post-snapshot WAL replay. The key invariant is that the receiving node never serves a read for a key before confirming it has received the snapshot chunk containing that key:

---- MODULE SnapshotTransfer ----
EXTENDS Naturals, FiniteSets, Sequences, TLC

CONSTANTS Nodes, Keys

VARIABLES
    nodeState,          \* nodeState[n] \in {"source", "receiving", "ready"}
    snapshotChunks,     \* snapshotChunks[n] = set of keys received so far
    keyData,            \* keyData[n][k] = value or "missing"
    transferLog         \* ordered sequence of chunks sent by source

\* A node only serves reads for keys it has fully received
ReadSafe(n, k) ==
    /\ nodeState[n] = "ready"
    /\ k \in snapshotChunks[n]

\* No key is "missing" in a ready node's snapshot
SnapshotComplete ==
    \A n \in Nodes :
        nodeState[n] = "ready" =>
            \A k \in Keys : k \in snapshotChunks[n]

====

Running TLC from a Makefile

# Makefile target for model checking
TLC     := java -jar $(TLA_TOOLS)/tla2tools.jar
WORKERS := $(shell nproc)

check-txn:
	$(TLC) -workers $(WORKERS) \
	       -config specs/TwoPhaseCommit.cfg \
	       -metadir /tmp/tlc-txn \
	       specs/TwoPhaseCommit.tla

check-split:
	$(TLC) -workers $(WORKERS) \
	       -config specs/ShardSplit.cfg \
	       -metadir /tmp/tlc-split \
	       specs/ShardSplit.tla

check-snapshot:
	$(TLC) -workers $(WORKERS) \
	       -config specs/SnapshotTransfer.cfg \
	       -metadir /tmp/tlc-snapshot \
	       specs/SnapshotTransfer.tla

validate-trace:
	go run ./cmd/tlavalidator \
	    -spec specs/TwoPhaseCommit.tla \
	    -log  /var/log/mydb/txn-trace.jsonl

Practical Applications

In a well-maintained distributed system, TLA+ specifications serve as the authoritative design documents for critical protocols such as distributed transactions, shard splits, and snapshot transfers. Each spec should be written before the corresponding implementation, with TLC run during development as a design-level test suite. Several classes of bug are found exclusively through model checking—they would have been invisible to integration tests because they require specific interleavings of concurrent operations that are unlikely to occur in a test environment but inevitable in production at scale.

The runtime trace validator runs as a nightly batch job against the previous day’s production logs. Each structured trace entry is parsed and checked against the specification’s Next relation. When the validator finds a violation, it produces a TLA+ counterexample trace showing the exact sequence of states that led to the invalid transition. This has proven more actionable than a raw stack trace because it shows the system-level causality (which transactions were in flight, which nodes had prepared) rather than just the local failure point.

The 86,000+ line specification corpus also serves as onboarding documentation. New engineers working on the transaction coordinator read the TLA+ spec before reading the Go implementation. Because TLA+ strips away language-level noise (goroutine lifecycle, error handling, logging) and expresses the protocol as a pure state machine, the spec communicates the essential design decisions—why the coordinator writes to the WAL before sending Prepare messages, why the abort path is idempotent—more clearly than inline comments in Go code.

Common Pitfalls

• Specifying implementation details instead of protocol properties — A TLA+ spec that mirrors Go struct layouts line-for-line is not useful. The spec should describe what the protocol must guarantee (atomicity, consistency), not how the implementation achieves it (mutex layout, channel buffer sizes). Over-specification produces a spec that is hard to model-check and does not generalize across implementation changes.
• State space explosion from unbound constants — Running TLC with RM = {r1, r2, r3, r4, r5} and no symmetry constraints can produce hundreds of billions of states. Always start with the minimum number of instances that exercises the protocol (2 RMs for two-phase commit, 2 shards for a split), add symmetry sets for interchangeable components, and use model constraints to bound sequences and message queues.
• Missing liveness conditions — A spec that only declares safety invariants can pass TLC even if the protocol can deadlock. Always include a fairness condition (WF_vars(Next) or SF_vars(CriticalAction)) and a liveness property that checks that the protocol makes progress. TLC’s deadlock detection is separate from liveness checking—enable both.
• Trace validator schema drift — The structured log schema emitted by the Go implementation must stay in sync with the variable names in the TLA+ spec. When a spec variable is renamed, the validator will silently ignore that variable, producing false negatives. Version the spec and the log schema together, and add a validator test that checks every spec variable has a corresponding log field.
• Forgetting to model message loss and duplication — A spec that assumes messages are delivered exactly once will not find the bugs that matter in real distributed systems. Add explicit MsgLost and MsgDuplicated actions to the network model. This doubles the state space but uncovers the redelivery handling bugs that cause production incidents.
• Not checking the refinement mapping — It is tempting to write a concrete spec and check it in isolation without verifying that it refines the abstract spec. Without a refinement proof, the concrete spec may satisfy its own invariants but violate the higher-level guarantee. TLC can check refinement automatically if the mapping is expressed as a THEOREM Concrete!Spec => Abstract!Spec with an explicit variable mapping.