Introduction

In 1999 Amazon engineers found fifteen bugs in real distributed-systems protocols — not by testing, but by writing TLA+ specifications. One was a data-loss bug that would have surfaced only under a rare combination of failures nobody had imagined.

TLA+ is a formal specification language invented by Leslie Lamport (the same Lamport behind Lamport clocks and the Paxos consensus protocol, awarded the Turing Award in 2013). It describes a system as a state machine: a set of variables holding the current state, an initial condition, and a collection of actions — guarded transitions that may update those variables. Every possible interleaving of actions across concurrent processes is explored automatically by a model checker called TLC.

The core insight is simple but powerful: if you can write down what a system is supposed to do (its invariant — a predicate that must hold in every reachable state), then a model checker can exhaustively verify it on all finite executions up to a bounded depth. Bugs that survive every unit test often die instantly against a spec.

Try It: State-Machine Explorer

Below is a miniature two-process mutual exclusion protocol — the classic problem of ensuring two concurrent processes never enter the critical section at the same time. Each process follows three steps: idle → waiting → critical. A flag variable controls who may proceed.

<!-- Two-process mutual exclusion state machine explorer -->
<div class="panel">
  <div class="spec-box">
    <div class="spec-title">SPEC: Two-Process Mutual Exclusion</div>
    <pre class="spec-code">VARIABLES pc, flag
Init == pc = [p \in {0,1} |-> "idle"] /\ flag = 0
SetFlag(i) == pc[i]="idle" /\ pc'=[pc EXCEPT ![i]="waiting"] /\ flag'=i
Enter(i)  == pc[i]="waiting" /\ flag=i /\ pc'=[pc EXCEPT ![i]="critical"] /\ UNCHANGED flag
Exit(i)   == pc[i]="critical" /\ pc'=[pc EXCEPT ![i]="idle"] /\ UNCHANGED flag
Next == \E i \in {0,1}: SetFlag(i) \/ Enter(i) \/ Exit(i)
Mutex == ~(pc[0]="critical" /\ pc[1]="critical")</pre>
  </div>
  <div class="controls">
    <button id="btn-step" type="button">Step</button>
    <button id="btn-bfs" type="button">BFS (check all)</button>
    <button id="btn-reset" type="button" class="ghost">Reset</button>
    <span class="inv-badge" id="inv-badge" title="Mutual exclusion invariant status">Mutex OK</span>
  </div>
  <div id="status-line" class="status-line"></div>
  <div id="state-grid" class="state-grid"></div>
</div>

/* Layout and state-card styles */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.panel { display: flex; flex-direction: column; gap: .6rem; padding: .4rem; }
.spec-box { background: #1e2433; border-radius: 8px; padding: .7rem 1rem; }
.spec-title { color: #8ec5fc; font-size: .78rem; font-weight: 600; letter-spacing: .04em; margin-bottom: .3rem; }
.spec-code { color: #e2e8f0; font: 13px/1.55 ui-monospace, monospace; margin: 0; white-space: pre-wrap; }
.controls { display: flex; align-items: center; gap: .4rem; flex-wrap: wrap; }
button { font: 600 13px system-ui; padding: .38rem .8rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 6px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .45; cursor: default; }
.inv-badge { margin-left: auto; font: 600 11px system-ui; padding: .22rem .55rem;
             border-radius: 20px; background: #d1fae5; color: #065f46; border: 1px solid #6ee7b7; }
.inv-badge.violated { background: #fee2e2; color: #991b1b; border-color: #fca5a5; }
.status-line { font-size: .88rem; font-weight: 600; min-height: 1.3em; color: #374151; }
.state-grid { display: flex; flex-wrap: wrap; gap: 6px; }
.state-card { border: 1.5px solid #cbd5e1; border-radius: 8px; padding: .4rem .55rem;
              font: 12px ui-monospace, monospace; background: #f8fafc; min-width: 130px; cursor: default; }
.state-card.current { border-color: #2563eb; background: #eff6ff; box-shadow: 0 0 0 2px #93c5fd44; }
.state-card.bad { border-color: #dc2626; background: #fef2f2; }
.state-card.visited { opacity: .55; }
.state-card .card-head { font-weight: 700; color: #1e40af; margin-bottom: .15rem; font-size: 11px; }
.state-card.bad .card-head { color: #dc2626; }
.state-card .card-line { color: #374151; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Model: two processes (0 and 1), each with a program counter pc[i]
// and a shared flag variable. A process sets the flag to itself before
// entering the critical section; it may only enter if the flag still
// points to it (Peterson-like, simplified to 2-state waiting).

const IDLE = 'idle', WAITING = 'waiting', CRITICAL = 'critical';

// State representation
function mkState(pc0, pc1, flag) { return { pc: [pc0, pc1], flag }; }
function stateKey(s) { return s.pc[0] + '|' + s.pc[1] + '|' + s.flag; }
function cloneState(s) { return mkState(s.pc[0], s.pc[1], s.flag); }

// Invariant: never both processes in critical at the same time
function mutexOk(s) { return !(s.pc[0] === CRITICAL && s.pc[1] === CRITICAL); }

// Generate all enabled transitions from a state
function successors(s) {
  const nexts = [];
  for (let i = 0; i < 2; i++) {
    const j = 1 - i;
    const ns = cloneState(s);
    if (s.pc[i] === IDLE) {
      // process i sets flag and moves to waiting
      ns.pc[i] = WAITING; ns.flag = i; nexts.push({ label: i18nFmt('P%i% sets flag', { i }), s: ns });
    } else if (s.pc[i] === WAITING && s.flag === i) {
      // process i enters critical if flag still points to it
      const ns2 = cloneState(s); ns2.pc[i] = CRITICAL; nexts.push({ label: i18nFmt('P%i% enters', { i }), s: ns2 });
    } else if (s.pc[i] === CRITICAL) {
      // process i exits and returns to idle
      const ns3 = cloneState(s); ns3.pc[i] = IDLE; nexts.push({ label: i18nFmt('P%i% exits', { i }), s: ns3 });
    }
  }
  return nexts;
}

let allStates = [];
let currentIdx = 0;
let bfsDone = false;
let violation = null;

function init() {
  const s0 = mkState(IDLE, IDLE, 0);
  allStates = [{ state: s0, from: -1, label: 'initial', depth: 0 }];
  currentIdx = 0; bfsDone = false; violation = null;
  render();
}

function stepOnce() {
  if (bfsDone) return;
  const cur = allStates[currentIdx];
  const nexts = successors(cur.state);
  if (nexts.length === 0) { bfsDone = true; render(); return; }
  // for Step mode just follow the first available transition
  const { label, s } = nexts[0];
  const key = stateKey(s);
  const existing = allStates.findIndex(e => stateKey(e.state) === key);
  if (existing === -1) {
    allStates.push({ state: s, from: currentIdx, label, depth: cur.depth + 1 });
    currentIdx = allStates.length - 1;
  } else {
    currentIdx = existing;
  }
  render();
}

function runBFS() {
  const seen = new Map();
  seen.set(stateKey(allStates[0].state), 0);
  const queue = [0];
  allStates = [allStates[0]];
  violation = null;
  let head = 0;
  while (head < queue.length) {
    const idx = queue[head++];
    const cur = allStates[idx];
    if (!mutexOk(cur.state)) { violation = idx; break; }
    for (const { label, s } of successors(cur.state)) {
      const k = stateKey(s);
      if (!seen.has(k)) {
        seen.set(k, allStates.length);
        allStates.push({ state: s, from: idx, label, depth: cur.depth + 1 });
        queue.push(allStates.length - 1);
      }
    }
  }
  bfsDone = true; currentIdx = violation !== null ? violation : allStates.length - 1;
  render();
}

function render() {
  const badge = document.getElementById('inv-badge');
  const statusEl = document.getElementById('status-line');
  if (violation !== null) {
    badge.textContent = 'Mutex VIOLATED'; badge.className = 'inv-badge violated';
    statusEl.textContent = i18nFmt('Invariant VIOLATED — counterexample found among %n% states.', { n: allStates.length });
  } else if (bfsDone) {
    badge.textContent = 'Mutex holds'; badge.className = 'inv-badge';
    statusEl.textContent = i18nFmt('BFS complete — %n% states explored, invariant holds.', { n: allStates.length });
  } else {
    badge.textContent = 'Mutex OK'; badge.className = 'inv-badge';
    statusEl.textContent = i18nFmt('Explored %n% state(s). Use BFS to check all.', { n: allStates.length });
  }
  document.getElementById('btn-step').disabled = bfsDone;
  document.getElementById('btn-bfs').disabled = bfsDone;

  const grid = document.getElementById('state-grid');
  grid.innerHTML = '';
  const show = allStates.slice(0, 30); // cap visible cards to avoid layout overflow
  show.forEach((entry, idx) => {
    const { state, label, depth } = entry;
    const isCur = idx === currentIdx;
    const isBad = !mutexOk(state);
    const card = document.createElement('div');
    card.className = 'state-card' + (isCur ? ' current' : '') + (isBad ? ' bad' : '') + (!isCur && !isBad && bfsDone ? ' visited' : '');
    const p0Label = 'P0';
    const p1Label = 'P1';
    card.innerHTML =
      '<div class="card-head">' + (isBad ? '! ' : '') + 'S' + idx + (label ? ' <span style="font-weight:400;color:#64748b">← ' + label + '</span>' : '') + '</div>' +
      '<div class="card-line">' + p0Label + ': ' + state.pc[0] + '</div>' +
      '<div class="card-line">' + p1Label + ': ' + state.pc[1] + '</div>' +
      '<div class="card-line">flag: ' + state.flag + '</div>';
    grid.appendChild(card);
  });
  if (allStates.length > 30) {
    const more = document.createElement('div');
    more.className = 'state-card visited';
    more.innerHTML = '<div class="card-head">' + i18nFmt('…%n% more states', { n: allStates.length - 30 }) + '</div>';
    grid.appendChild(more);
  }
}

document.getElementById('btn-step').addEventListener('click', stepOnce);
document.getElementById('btn-bfs').addEventListener('click', runBFS);
document.getElementById('btn-reset').addEventListener('click', init);
init();
Result
Console

The explorer shows every reachable state. Step advances one transition; BFS explores all states up to a depth limit and highlights any state where the mutual-exclusion invariant is violated (both processes in the critical section simultaneously). A correct protocol finds zero violations; a broken one shows the exact counterexample path.

The Real Complexity

TLA+ looks deceptively simple — a few variable declarations, an initial predicate, a next-state relation. The hidden cost is the state space.

  • State explosion. Two Boolean variables give 22=42^{2} = 4 states. Ten variables give 210=1,0242^{10} = 1{,}024. Ten concurrent processes each with ten Boolean variables give 21002^{100} — more than atoms in the observable universe.
  • Model checking is PSPACE-complete. Verifying a linear temporal logic (LTL) property over all executions of a finite-state system is known to be in PSPACE (Sistla and Clarke, 1985) and hard for PSPACE. In practice, TLC uses breadth-first search and clever symmetry reductions, but exponential blow-up is the fundamental enemy.
  • Liveness is harder. Safety properties ("nothing bad ever happens") reduce to reachability — already hard. Liveness properties ("something good eventually happens") require checking for infinite fair executions and push the problem into the realm of omega-automata.
  • The state-space bound pays off. Unlike testing — which samples executions — model checking is exhaustive up to the model's bound. Finding a bug means producing a concrete counterexample trace, not a probabilistic report.

The implication: TLA+ is most effective on the core protocol logic of a system, not on the full production codebase. Engineers write a small spec capturing the tricky concurrent invariant, model-check it, then implement with confidence.

Where It Matters

TLA+ is not an academic curiosity — it is in production at some of the world's largest software companies:

  • Amazon Web Services: engineers have written TLA+ specs for S3, DynamoDB, EBS, and dozens of internal services. The 2014 paper How Amazon Web Services Uses Formal Methods reported that TLC found bugs in every non-trivial spec they wrote.
  • Microsoft Azure Cosmos DB: the team used TLA+ to verify the multi-master replication protocol; without it, subtle races across replica failover would have been nearly impossible to find by testing alone.
  • Apache Kafka: the distributed log's leader-election and log-replication protocols have been specified and model-checked in TLA+.
  • Intel and semiconductor design: hardware memory-model specifications for x86 and ARM are studied in TLA+ variants; a memory model bug can affect billions of chips.

Beyond industry, TLA+ connects to deep theory. Its invariant-checking core is the same reachability problem that makes P vs NP relevant: any NP-hard problem can be encoded as "does this state machine reach a bad state?" And its liveness fragment touches the boundary of the halting problem.

Conclusion

TLA+ asks a disarmingly modest question: can you write down what your system is supposed to do? If you can — even for just the tricky concurrent core — a model checker will explore every execution and hand you a counterexample the moment an invariant breaks.

The cost is real: state explosion is exponential, and there is no free lunch between expressiveness and tractability. But for the class of bugs that live in the interaction between concurrent processes — the race conditions, the partial-failure corner cases, the subtle protocol violations — no amount of testing reaches the same guarantee. A spec written before the code is a contract; a model checker is the machine that holds both sides to it.

Next time a distributed system misbehaves in production, ask whether a 30-line TLA+ spec might have found it first. Lamport's answer, backed by Amazon's fifteen-bug count, is: almost certainly yes.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/tla-plus-specs/Content licensed under CC BY-NC 4.0.