home > research > tla-plus-system-design > index (2026-01-11)

TLA+ for System Design: A CTO/L7 Engineer's Guide

TLA+ for System Design: A CTO/L7 Engineer's Guide

Table of Contents

Overview

TLA+ (Temporal Logic of Actions) is a formal specification language for designing, modeling, and verifying concurrent and distributed systems. Created by Leslie Lamport (Turing Award 2013), TLA+ enables engineers to catch critical design bugs before writing any implementation code.

Why TLA+ Matters for System Design

At scale, distributed systems exhibit behaviors that are nearly impossible to reason about through code review or traditional testing:

  • Race conditions that manifest once per million requests
  • Deadlocks that occur only under specific failure sequences
  • Data corruption from unexpected state interleaving
  • Protocol bugs that violate safety invariants

TLA+ addresses these by enabling exhaustive exploration of the state space before implementation.

The Business Case

Problem Traditional Approach TLA+ Approach
Design validation Code review, testing Mathematical proof
Edge case discovery Production incidents Model checking
Documentation Prose that diverges Executable specs
Team alignment Meetings, diagrams Formal shared model
Confidence level "Probably works" "Verified correct"

Amazon's experience: Engineers reported that TLA+ helped them find subtle bugs in DynamoDB, S3, and EBS that would have been extremely difficult to catch otherwise, potentially preventing costly outages.

Background and History

Leslie Lamport and Formal Methods

Leslie Lamport developed TLA+ beginning in 1994, building on decades of work in distributed systems theory:

  • 1978: Lamport introduces "Time, Clocks, and the Ordering of Events" - foundational work on logical clocks
  • 1982: Byzantine fault tolerance (Lamport, Shostak, Pease)
  • 1989: Paxos consensus algorithm (published 1998)
  • 1994: TLA (Temporal Logic of Actions) introduced
  • 1999: TLA+ specification language and tooling
  • 2009: PlusCal algorithmic language added
  • 2013: Lamport receives Turing Award

Relationship to Formal Methods

TLA+ sits in the practical middle ground of formal verification: 

                    Rigor
                      ▲
                      │
    Theorem Provers   │   Coq, Isabelle/HOL, Lean
    (Full proofs)     │   ────────────────────────
                      │
    Model Checking    │   TLA+, Alloy, SPIN
    (Exhaustive)      │   ────────────────────────
                      │
    Property Testing  │   QuickCheck, Hypothesis
    (Randomized)      │   ────────────────────────
                      │
    Unit Testing      │   JUnit, pytest
    (Examples)        │
                      └──────────────────────────▶ Ease of Use

TLA+ optimizes for practical verification of system designs rather than full mathematical proofs, making it accessible to working engineers.

Key Concepts

State Machines and Behaviors

TLA+ models systems as state machines. A behavior is an infinite sequence of states: 

State₀ → State₁ → State₂ → State₃ → ...

Each transition represents an atomic action that changes the system state. 

---- MODULE Counter ----
VARIABLE count

Init == count = 0

Increment == count' = count + 1

Decrement == count > 0 /\ count' = count - 1

Next == Increment \/ Decrement

Spec == Init /\ [][Next]_count
====

Key elements:

  • VARIABLE: Declares state variables
  • Init: Initial state predicate
  • Next: Transition relation (what can happen)
  • Spec: Complete specification (init + behavior)
  • Primed variables (count'): Next-state values

Temporal Logic

TLA+ uses temporal operators to express properties over behaviors:

Operator Meaning Example
[]P Always P (safety) [](count >= 0)
<>P Eventually P (liveness) <>(count = 10)
[]<>P Infinitely often P []<>(enabled)
<>[]P Eventually always P <>[](stable)
P ~> Q P leads to Q request ~> response

Safety vs. Liveness Properties

Safety: "Nothing bad ever happens"

  • Type invariants
  • Mutual exclusion
  • Data consistency

Liveness: "Something good eventually happens"

  • Requests get responses
  • Messages are delivered
  • Processes terminate
\* Safety: Account balance never goes negative
TypeInvariant == balance >= 0

\* Liveness: Every withdrawal request eventually completes
Liveness == \A r \in requests : <>(r.completed)

Specification vs. Implementation

TLA+ specifications are not programs. They describe what a system does, not how:

Specification (TLA+) Implementation (Code)
Abstract state Concrete data structures
Non-determinism Specific choices
Atomic actions Multiple instructions
Infinite behaviors Actual execution
Mathematical sets Arrays, hash maps

This abstraction is a feature: it lets you reason about essential correctness without implementation details.

Model Checking with TLC

TLC (TLA+ Model Checker) exhaustively explores the state space:

  1. Start from initial states
  2. Apply all enabled actions
  3. Check invariants at each state
  4. Track visited states (no infinite loops)
  5. Report any property violations
┌────────────────────────────────────────────────────┐
│                  State Space                        │
│                                                     │
│    S₀ ──▶ S₁ ──▶ S₄                               │
│     │      │      │                                 │
│     ▼      ▼      ▼                                 │
│    S₂ ──▶ S₃ ──▶ S₅ ◀── Invariant violation!      │
│                  ▲                                  │
│                  │                                  │
│           Error trace provided                      │
│                                                     │
└────────────────────────────────────────────────────┘

TLC features:

  • Symmetric model symmetry optimization
  • Multi-threaded exploration
  • Distributed checking across machines
  • Counterexample traces for debugging

PlusCal: Higher-Level Syntax

PlusCal is an algorithmic language that compiles to TLA+, making specifications more accessible: 

---- MODULE TransferPlusCal ----
EXTENDS Integers, TLC

CONSTANTS Accounts, InitBalance

(*--algorithm Transfer
variables
    balance = [a \in Accounts |-> InitBalance];

define
    TotalConstant ==
        LET Sum(S) == IF S = {} THEN 0
                      ELSE LET x == CHOOSE x \in S : TRUE
                           IN balance[x] + Sum(S \ {x})
        IN Sum(Accounts) = Cardinality(Accounts) * InitBalance
end define;

process Transfer \in 1..3
variables from, to, amount;
begin
    ChooseAccounts:
        from := CHOOSE a \in Accounts : TRUE;
        to := CHOOSE a \in Accounts : a /= from;
        amount := CHOOSE n \in 1..balance[from] : TRUE;
    DoTransfer:
        if balance[from] >= amount then
            balance[from] := balance[from] - amount;
            balance[to] := balance[to] + amount;
        end if;
end process;

end algorithm; *)
====

PlusCal advantages:

  • Familiar imperative syntax
  • Labels define atomicity
  • Processes model concurrency
  • Compiles to readable TLA+

Common Patterns and Specifications

Two-Phase Commit

---- MODULE TwoPhaseCommit ----
EXTENDS Integers, FiniteSets

CONSTANTS RM  \* Resource Managers

VARIABLES
    rmState,      \* State of each RM
    tmState,      \* State of Transaction Manager
    tmPrepared,   \* RMs that have prepared
    msgs          \* Messages in transit

vars == <<rmState, tmState, tmPrepared, msgs>>

Message == [type: {"Prepare", "Commit", "Abort", "Prepared", "Aborted"}]

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

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

\* Transaction Manager sends Prepare to all RMs
TMPrepare ==
    /\ tmState = "init"
    /\ tmState' = "preparing"
    /\ msgs' = msgs \cup {[type |-> "Prepare"]}
    /\ UNCHANGED <<rmState, tmPrepared>>

\* RM receives Prepare and responds
RMPrepare(r) ==
    /\ rmState[r] = "working"
    /\ [type |-> "Prepare"] \in msgs
    /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
    /\ msgs' = msgs \cup {[type |-> "Prepared"]}
    /\ UNCHANGED <<tmState, tmPrepared>>

\* RM can choose to abort
RMChooseAbort(r) ==
    /\ rmState[r] = "working"
    /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
    /\ msgs' = msgs \cup {[type |-> "Aborted"]}
    /\ UNCHANGED <<tmState, tmPrepared>>

\* TM receives Prepared from RM
TMRcvPrepared(r) ==
    /\ tmState = "preparing"
    /\ [type |-> "Prepared"] \in msgs
    /\ tmPrepared' = tmPrepared \cup {r}
    /\ IF tmPrepared' = RM
       THEN /\ tmState' = "committed"
            /\ msgs' = msgs \cup {[type |-> "Commit"]}
       ELSE /\ UNCHANGED tmState
            /\ UNCHANGED msgs
    /\ UNCHANGED rmState

\* TM receives Aborted and aborts transaction
TMRcvAborted ==
    /\ tmState = "preparing"
    /\ [type |-> "Aborted"] \in msgs
    /\ tmState' = "aborted"
    /\ msgs' = msgs \cup {[type |-> "Abort"]}
    /\ UNCHANGED <<rmState, tmPrepared>>

\* RM commits
RMCommit(r) ==
    /\ rmState[r] = "prepared"
    /\ [type |-> "Commit"] \in msgs
    /\ rmState' = [rmState EXCEPT ![r] = "committed"]
    /\ UNCHANGED <<tmState, tmPrepared, msgs>>

\* RM aborts
RMAbort(r) ==
    /\ rmState[r] \in {"working", "prepared"}
    /\ [type |-> "Abort"] \in msgs
    /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
    /\ UNCHANGED <<tmState, tmPrepared, msgs>>

Next ==
    \/ TMPrepare
    \/ TMRcvAborted
    \/ \E r \in RM :
        \/ RMPrepare(r)
        \/ RMChooseAbort(r)
        \/ TMRcvPrepared(r)
        \/ RMCommit(r)
        \/ RMAbort(r)

\* Safety: No RM commits if any RM aborts
Consistency ==
    \A r1, r2 \in RM :
        ~ (rmState[r1] = "committed" /\ rmState[r2] = "aborted")

Spec == Init /\ [][Next]_vars

THEOREM Spec => []Consistency
====

Distributed Lock (Lease-Based)

---- MODULE DistributedLock ----
EXTENDS Integers, Naturals

CONSTANTS
    Nodes,        \* Set of nodes
    MaxTime       \* Maximum simulation time

VARIABLES
    lock,         \* Current lock holder (or "none")
    leaseEnd,     \* When current lease expires
    time,         \* Global logical time
    requests      \* Pending lock requests

vars == <<lock, leaseEnd, time, requests>>

TypeOK ==
    /\ lock \in Nodes \cup {"none"}
    /\ leaseEnd \in 0..MaxTime
    /\ time \in 0..MaxTime
    /\ requests \subseteq Nodes

Init ==
    /\ lock = "none"
    /\ leaseEnd = 0
    /\ time = 0
    /\ requests = {}

\* Node requests the lock
Request(n) ==
    /\ n \notin requests
    /\ requests' = requests \cup {n}
    /\ UNCHANGED <<lock, leaseEnd, time>>

\* Lock is granted with a lease
Grant(n, duration) ==
    /\ n \in requests
    /\ \/ lock = "none"
       \/ time >= leaseEnd  \* Lease expired
    /\ lock' = n
    /\ leaseEnd' = time + duration
    /\ requests' = requests \ {n}
    /\ UNCHANGED time

\* Node releases lock early
Release(n) ==
    /\ lock = n
    /\ lock' = "none"
    /\ leaseEnd' = time
    /\ UNCHANGED <<time, requests>>

\* Time advances
Tick ==
    /\ time < MaxTime
    /\ time' = time + 1
    /\ UNCHANGED <<lock, leaseEnd, requests>>

\* Lease expires
Expire ==
    /\ lock /= "none"
    /\ time >= leaseEnd
    /\ lock' = "none"
    /\ UNCHANGED <<leaseEnd, time, requests>>

Next ==
    \/ \E n \in Nodes : Request(n)
    \/ \E n \in Nodes, d \in 1..5 : Grant(n, d)
    \/ \E n \in Nodes : Release(n)
    \/ Tick
    \/ Expire

\* Safety: At most one node holds the lock at any time
MutualExclusion ==
    \A n1, n2 \in Nodes :
        (lock = n1 /\ lock = n2) => n1 = n2

\* Liveness: Every request is eventually granted
EventualGrant ==
    \A n \in Nodes :
        (n \in requests) ~> (lock = n)

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
====

Message Queue with Ordering

---- MODULE OrderedQueue ----
EXTENDS Sequences, Integers, FiniteSets

CONSTANTS
    Producers,    \* Set of producer processes
    Consumers,    \* Set of consumer processes
    MaxQueueLen   \* Maximum queue length

VARIABLES
    queue,        \* The message queue
    produced,     \* Messages produced by each producer
    consumed,     \* Messages consumed by each consumer
    nextSeq       \* Next sequence number per producer

vars == <<queue, produced, consumed, nextSeq>>

Message == [producer: Producers, seq: Nat, data: Nat]

TypeOK ==
    /\ queue \in Seq(Message)
    /\ Len(queue) <= MaxQueueLen
    /\ produced \in [Producers -> Seq(Message)]
    /\ consumed \in [Consumers -> Seq(Message)]
    /\ nextSeq \in [Producers -> Nat]

Init ==
    /\ queue = <<>>
    /\ produced = [p \in Producers |-> <<>>]
    /\ consumed = [c \in Consumers |-> <<>>]
    /\ nextSeq = [p \in Producers |-> 1]

\* Producer sends a message
Produce(p, data) ==
    /\ Len(queue) < MaxQueueLen
    /\ LET msg == [producer |-> p, seq |-> nextSeq[p], data |-> data]
       IN /\ queue' = Append(queue, msg)
          /\ produced' = [produced EXCEPT ![p] = Append(@, msg)]
          /\ nextSeq' = [nextSeq EXCEPT ![p] = @ + 1]
    /\ UNCHANGED consumed

\* Consumer receives a message (FIFO)
Consume(c) ==
    /\ Len(queue) > 0
    /\ LET msg == Head(queue)
       IN /\ queue' = Tail(queue)
          /\ consumed' = [consumed EXCEPT ![c] = Append(@, msg)]
    /\ UNCHANGED <<produced, nextSeq>>

Next ==
    \/ \E p \in Producers, d \in 1..10 : Produce(p, d)
    \/ \E c \in Consumers : Consume(c)

\* Safety: FIFO ordering is preserved per producer
FIFOOrdering ==
    \A c \in Consumers :
        \A i, j \in 1..Len(consumed[c]) :
            (i < j /\ consumed[c][i].producer = consumed[c][j].producer)
            => consumed[c][i].seq < consumed[c][j].seq

\* Safety: No message duplication
NoDuplication ==
    \A c1, c2 \in Consumers :
        \A i \in 1..Len(consumed[c1]) :
            \A j \in 1..Len(consumed[c2]) :
                (c1 /= c2 \/ i /= j) =>
                    consumed[c1][i] /= consumed[c2][j]

Spec == Init /\ [][Next]_vars

THEOREM Spec => [](FIFOOrdering /\ NoDuplication)
====

Raft Consensus (Simplified)

---- MODULE RaftLeaderElection ----
EXTENDS Integers, FiniteSets

CONSTANTS
    Server,       \* Set of servers
    MaxTerm       \* Maximum term for model checking

VARIABLES
    currentTerm,  \* Current term for each server
    votedFor,     \* Who this server voted for in current term
    state,        \* follower, candidate, or leader
    votesGranted  \* Votes received by candidates

vars == <<currentTerm, votedFor, state, votesGranted>>

Quorum == {Q \in SUBSET Server : Cardinality(Q) * 2 > Cardinality(Server)}

TypeOK ==
    /\ currentTerm \in [Server -> 0..MaxTerm]
    /\ votedFor \in [Server -> Server \cup {NONE}]
    /\ state \in [Server -> {"follower", "candidate", "leader"}]
    /\ votesGranted \in [Server -> SUBSET Server]

Init ==
    /\ currentTerm = [s \in Server |-> 0]
    /\ votedFor = [s \in Server |-> NONE]
    /\ state = [s \in Server |-> "follower"]
    /\ votesGranted = [s \in Server |-> {}]

\* Server times out and starts election
StartElection(s) ==
    /\ state[s] \in {"follower", "candidate"}
    /\ currentTerm[s] < MaxTerm
    /\ currentTerm' = [currentTerm EXCEPT ![s] = @ + 1]
    /\ state' = [state EXCEPT ![s] = "candidate"]
    /\ votedFor' = [votedFor EXCEPT ![s] = s]
    /\ votesGranted' = [votesGranted EXCEPT ![s] = {s}]

\* Server grants vote to candidate
RequestVote(candidate, voter) ==
    /\ state[candidate] = "candidate"
    /\ currentTerm[candidate] >= currentTerm[voter]
    /\ \/ votedFor[voter] = NONE
       \/ votedFor[voter] = candidate
    /\ currentTerm' = [currentTerm EXCEPT ![voter] = currentTerm[candidate]]
    /\ votedFor' = [votedFor EXCEPT ![voter] = candidate]
    /\ votesGranted' = [votesGranted EXCEPT ![candidate] = @ \cup {voter}]
    /\ state' = [state EXCEPT ![voter] = IF currentTerm[voter] < currentTerm[candidate]
                                          THEN "follower" ELSE @]

\* Candidate wins election
BecomeLeader(s) ==
    /\ state[s] = "candidate"
    /\ votesGranted[s] \in Quorum
    /\ state' = [state EXCEPT ![s] = "leader"]
    /\ UNCHANGED <<currentTerm, votedFor, votesGranted>>

\* Server discovers higher term
StepDown(s, term) ==
    /\ term > currentTerm[s]
    /\ currentTerm' = [currentTerm EXCEPT ![s] = term]
    /\ state' = [state EXCEPT ![s] = "follower"]
    /\ votedFor' = [votedFor EXCEPT ![s] = NONE]
    /\ UNCHANGED votesGranted

Next ==
    \/ \E s \in Server : StartElection(s)
    \/ \E c, v \in Server : RequestVote(c, v)
    \/ \E s \in Server : BecomeLeader(s)
    \/ \E s \in Server, t \in 1..MaxTerm : StepDown(s, t)

\* Safety: At most one leader per term
ElectionSafety ==
    \A s1, s2 \in Server :
        (state[s1] = "leader" /\ state[s2] = "leader" /\
         currentTerm[s1] = currentTerm[s2])
        => s1 = s2

Spec == Init /\ [][Next]_vars

THEOREM Spec => []ElectionSafety
====

Real-World Industry Applications

Amazon Web Services

Amazon has been one of the most vocal proponents of TLA+ in industry. Their 2015 paper "How Amazon Web Services Uses Formal Methods" describes extensive use:

DynamoDB

  • Verified replication protocol correctness
  • Found subtle bugs in the original design
  • Caught edge cases in failure recovery

"We discovered two bugs in the replication protocol. One of these bugs was subtle and would have been extremely difficult to find through any technique other than formal methods." – Amazon DynamoDB team

S3 (Simple Storage Service)

  • Modeled internal consistency protocols
  • Verified garbage collection doesn't delete live data
  • Caught concurrency bugs in background processes

EBS (Elastic Block Store)

  • Verified snapshot consistency
  • Modeled replication across availability zones
  • Found bugs in volume migration logic

Internal Tooling

Amazon built internal tools around TLA+:

  • IDE integration with their development environment
  • CI/CD integration for spec checking
  • Training programs for engineers

Microsoft

Azure Cosmos DB

Microsoft used TLA+ extensively for Cosmos DB's global distribution:

  • Five consistency levels formally verified
  • Conflict resolution protocols modeled
  • Partition split operations validated

"TLA+ helped us gain confidence that our consistency model implementations match their formal specifications." – Azure Cosmos DB team

Xbox Live

  • Modeled multiplayer game state synchronization
  • Verified matchmaking queue fairness
  • Validated anti-cheat detection timing

Other Microsoft Products

  • Azure Storage
  • Coyote (previously P#) - C# concurrency testing
  • Service Fabric distributed systems

Elasticsearch

Elasticsearch used TLA+ for their distributed replication:

  • Primary-backup replication protocol
  • Cluster state management
  • Shard allocation decisions

They open-sourced their specifications, providing valuable learning resources.

MongoDB

MongoDB employed TLA+ for:

  • Replica set elections
  • Sharding protocol changes
  • Transaction isolation verification

CockroachDB

CockroachDB (distributed SQL database) uses TLA+ for:

  • Raft consensus implementation
  • Distributed transaction protocols
  • Schema change coordination

Other Notable Users

Company Use Case
Confluent Kafka replication protocol
PingCAP TiDB distributed transactions
Thales Safety-critical embedded systems
Intel Cache coherence protocols

Tools and Ecosystem

TLA+ Toolbox

The official IDE for TLA+:

  • Spec editor with syntax highlighting
  • TLC model checker integration
  • TLAPS proof assistant integration
  • Trace explorer for counterexamples

Download: https://lamport.azurewebsites.net/tla/toolbox.html

VS Code Extensions

TLA+ Nightly (recommended)

Extension ID: alygin.vscode-tlaplus

Features:

  • Syntax highlighting
  • TLC integration
  • PlusCal translation
  • Error diagnostics
  • Code snippets

TLA+ (Official Microsoft)

Extension ID: alygin.vscode-tlaplus-nightly

More experimental features, faster updates.

TLC Model Checker

TLC is the workhorse of TLA+ verification: 

# Run model checker from command line
java -jar tla2tools.jar -modelcheck YourSpec.tla

# With configuration file
java -jar tla2tools.jar -modelcheck -config YourSpec.cfg YourSpec.tla

# Distributed mode (multiple workers)
java -jar tla2tools.jar -modelcheck -workers 4 YourSpec.tla

Configuration file (.cfg): 

SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT Safety
PROPERTY Liveness

CONSTANT
    Nodes = {n1, n2, n3}
    MaxMessages = 5

TLAPS (TLA+ Proof System)

For when model checking isn't enough (infinite state spaces): 

THEOREM TypeCorrect == Spec => []TypeOK
  <1>1. Init => TypeOK
    BY DEF Init, TypeOK
  <1>2. TypeOK /\ [Next]_vars => TypeOK'
    <2>1. CASE Action1
      BY <2>1 DEF TypeOK, Action1
    <2>2. CASE Action2
      BY <2>2 DEF TypeOK, Action2
    <2>3. CASE UNCHANGED vars
      BY <2>3 DEF TypeOK
    <2>4. QED
      BY <2>1, <2>2, <2>3 DEF Next
  <1>3. QED
    BY <1>1, <1>2, PTL DEF Spec

TLAPS integrates with SMT solvers (Z3, CVC4) and proof assistants (Isabelle).

Apalache: Symbolic Model Checker

Apalache is a modern symbolic model checker for TLA+:

  • Bounded model checking
  • Handles larger state spaces than TLC
  • Type inference and checking
  • SMT-based verification
# Type checking
apalache-mc typecheck YourSpec.tla

# Bounded model checking
apalache-mc check --length=10 YourSpec.tla

# Check specific invariant
apalache-mc check --inv=Safety YourSpec.tla

Advantages over TLC:

  • Better handling of integer arithmetic
  • Symbolic exploration (not explicit enumeration)
  • Type annotations for clarity

Formal Verification Tool Comparison

Tool Approach Strengths Limitations
TLC Explicit model checking Complete exploration Memory bound
Apalache Symbolic/SMT Large state spaces Bounded depth
TLAPS Theorem proving Infinite systems Manual effort

Complementary Tools

Alloy

Lightweight formal modeling, good for data models: 

sig Node {
    neighbors: set Node
}

fact symmetric {
    all n1, n2: Node | n1 in n2.neighbors <=> n2 in n1.neighbors
}

pred connected {
    all n1, n2: Node | n1 in n2.^neighbors
}

run connected for 5 Node

SPIN/Promela

Process algebra approach, good for protocol verification: 

mtype = { request, response };
chan channel = [10] of { mtype, int };

proctype Client(int id) {
    channel ! request, id;
    channel ? response, id;
}

Learning Resources

Official Resources

Lamport's TLA+ Video Course

The TLA+ Video Course by Leslie Lamport himself:

  • 10+ hours of video lectures
  • Starts from basics
  • Covers PlusCal and TLC
  • Free on Lamport's website

Highly recommended as the authoritative introduction.

TLA+ Home Page

https://lamport.azurewebsites.net/tla/tla.html

  • Language reference
  • Tool downloads
  • Example specifications
  • Research papers

Books

Practical TLA+ (Hillel Wayne)

Practical TLA+: Planning Driven Development (Apress, 2018)

  • Practical, example-driven approach
  • Focuses on software engineers (not academics)
  • Real-world scenarios
  • PlusCal-first teaching

This is the most accessible book for working engineers.

Specifying Systems (Lamport)

Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

  • Free PDF available
  • Comprehensive reference
  • More theoretical depth
  • Complete language specification

Online Resources

Learn TLA+

https://learntla.com/

Hillel Wayne's online tutorial:

  • Interactive examples
  • Progressive difficulty
  • Modern tooling focus

TLA+ Community Resources

https://github.com/tlaplus

  • Example specifications
  • Tool source code
  • Community contributions

Dr. TLA+ Series

Video series covering specific algorithms:

  • Paxos
  • Raft
  • Two-Phase Commit
  • Byzantine Paxos

https://github.com/drtla/doc

Papers and Articles

Essential Papers

  1. "How Amazon Web Services Uses Formal Methods" (2015)
  2. "Use of Formal Methods at Amazon Web Services" (2014)
  3. "The TLA+ Proof System: Building a Heterogeneous Verification Platform" (2012)
    • TLAPS architecture paper

Blog Posts and Tutorials

Community

TLA+ Google Group

https://groups.google.com/g/tlaplus

Active community, Lamport occasionally participates.

TLA+ Discord/Slack

Community chat channels for real-time help.

Conferences

  • Strange Loop (frequent TLA+ talks)
  • PODC (Principles of Distributed Computing)
  • DISC (Distributed Computing)

Getting Started: A Practical Path

Week 1-2: Foundations

  1. Watch Lamport's Video Course (Lectures 1-5)
  2. Install TLA+ Toolbox
  3. Work through Die Hard example
  4. Read "Practical TLA+" Chapters 1-3

Week 3-4: Core Concepts

  1. Complete video course
  2. Model a simple protocol (mutex, producer-consumer)
  3. Learn PlusCal syntax
  4. Run TLC model checker

Week 5-6: Real Applications

  1. Study Amazon's published specs
  2. Model a system from your own work
  3. Learn to interpret counterexamples
  4. Practice finding bugs intentionally

Week 7-8: Advanced Topics

  1. Temporal properties and liveness
  2. TLAPS basics (optional)
  3. Apalache for larger state spaces
  4. Review industry case studies

Ongoing Practice

  • Spec new designs before implementing
  • Keep a library of reusable patterns
  • Share specs for code review
  • Mentor others

Integration with Development Workflow

When to Use TLA+

TLA+ is most valuable for:

Good Fit Poor Fit
Distributed protocols CRUD applications
Consensus algorithms UI logic
Concurrency primitives Single-threaded code
Failure handling Well-understood patterns
Critical infrastructure Rapid prototypes

Design Phase Integration

┌─────────────────────────────────────────────────────────┐
│                   Design Process                        │
│                                                         │
│  Requirements ──▶ Informal Design ──▶ TLA+ Spec         │
│       │                                   │             │
│       │                                   ▼             │
│       │                            Model Checking       │
│       │                                   │             │
│       │              ┌────────────────────┼────────┐    │
│       │              │                    │        │    │
│       │         Bug Found?           Verified      │    │
│       │              │                    │        │    │
│       │              ▼                    ▼        │    │
│       │         Fix Design          Implementation │    │
│       │              │                    │        │    │
│       │              └────────────────────┘        │    │
│       │                                            │    │
│       └────────────────────────────────────────────┘    │
│                                                         │
└─────────────────────────────────────────────────────────┘

CI/CD Integration

# .github/workflows/tla-check.yml
name: TLA+ Model Checking

on:
  push:
    paths:
      - 'specs/**/*.tla'
      - 'specs/**/*.cfg'

jobs:
  model-check:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install TLA+ Tools
        run: |
          wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar

      - name: Run TLC
        run: |
          for spec in specs/*.tla; do
            java -jar tla2tools.jar -modelcheck "$spec"
          done

Documentation as Specification

TLA+ specs serve as executable documentation: 

docs/
├── architecture.md      # High-level overview
├── protocols/
│   ├── replication.tla  # Formal spec
│   ├── replication.cfg  # Model config
│   └── replication.md   # Plain English explanation
└── decisions/
    └── ADR-001-consistency-model.md

Deep Dive Examples

Explore complete TLA+ specifications for common system design patterns:

Conclusion

TLA+ represents a powerful tool for building reliable distributed systems. While it requires investment to learn, the return is substantial:

  • Catch bugs before implementation: Find design flaws when they're cheap to fix
  • Build confidence: Know your system handles edge cases
  • Improve communication: Specs are precise, executable documentation
  • Learn deeply: Formal modeling forces rigorous thinking

For CTOs and senior engineers, TLA+ is increasingly table stakes for critical infrastructure. Amazon, Microsoft, and other industry leaders have demonstrated that formal methods are practical and valuable in production systems.

The key insight: TLA+ doesn't replace testing or code review. It operates at a different level, verifying the design is correct before you write the code that implements it.

"TLA+ won't find the bug in your code. It will find the bug in your design." – Leslie Lamport (paraphrased)

References

Core References

  • Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.
  • Wayne, H. (2018). Practical TLA+: Planning Driven Development. Apress.
  • Newcombe, C., et al. (2015). How Amazon Web Services Uses Formal Methods. CACM.

Industry Case Studies

  • Amazon DynamoDB formal specification
  • Microsoft Azure Cosmos DB consistency proofs
  • Elasticsearch replication protocol specs
  • CockroachDB Raft implementation

Learning Paths

Author: Jason Walsh

j@wal.sh

Last Updated: 2026-01-11 19:03:20

build: 2026-01-11 19:06 | sha: 12a5c39