Chapter 7: Specifying Time — Introduction to TLA+

Translation status: Partial. Reviewed against Japanese source commit 910a6c5903cc on 2026-07-19. Some content, headings, examples, tables, or references remain partially synchronized. Track the remaining work.

7.1 The Challenge of Distributed Systems: Time and State Become Complex

The Fundamental Difficulty of Distribution

Distributed systems are one of the key technical foundations of modern digital society, but their design and implementation involve difficulties that are qualitatively different from those of a single-machine system. Those difficulties arise because physical constraints and logical constraints interact in complicated ways.

The most fundamental problem is the ambiguity of time. In a single machine, the execution order of instructions is largely deterministic, so the statement “A executed before B” has a clear meaning. In a distributed system, however, the temporal order between operations running on different machines is not obvious.

The Limits of Physical Time

Each machine has its own local clock, and perfect synchronization among those clocks is impossible. Relativity already tells us that absolute simultaneity is not a physically meaningful concept. Even at a practical engineering level, network delay, clock skew, and timezone differences make it hard to share one precise notion of time.

Suppose two servers, one in Tokyo and one in New York, each execute an operation at “12:00:00.000” according to their own clocks. Were those actions truly simultaneous? Once we account for timezone offsets, network delay, and clock precision, the answer becomes uncertain.

Increasing Complexity of Causality

In a distributed system, causal relationships among events become more subtle. For event A to be the cause of event B, information about A must have reached B. Because information propagation takes time, physical timestamps alone are not enough.

【擬似記法】

Node 1: event A occurs → send message
         |
         ↓ (network delay)
Node 2: receive message → event B occurs

To reason about such situations, we need a notion of logical time, not just physical time.

The Reality of Partial Failure

Partial failure is unavoidable in distributed systems. One part of the system may fail while the rest continues to operate. This is very different from the usual failure mode of a single-machine program.

Typical examples of partial failure include the following.

• Network partition: communication between some nodes is lost.
• Node failure: a particular machine stops responding.
• Performance degradation: one part of the system becomes much slower.
• Byzantine failure: a node behaves arbitrarily or maliciously.

Maintaining consistency under such conditions is one of the core design problems of distributed systems.

The Trade-Off Between Consistency and Availability

One of the most important results in distributed-systems theory is the CAP theorem as formalized by Gilbert and Lynch. The theorem assumes an asynchronous model in which a network partition may cause message loss. Under that assumption, an execution experiencing a partition cannot guarantee both of the following.

• Consistency: atomic, or linearizable, behavior in which each operation appears to take effect at one point between its invocation and response.
• Availability: every request received by a non-failing node eventually receives a response.

Here, partition tolerance is not a third guarantee to maximize independently; it is the assumption that the model permits such partitions.

CAP is therefore not a rule that a system must choose one of three letters at all times. During a partition, a request may be delayed or rejected to preserve linearizability, or it may be answered while temporarily providing a weaker consistency model. The relevant operations, failure and communication model, and required consistency level must be stated explicitly.

Managing Nondeterminism

Nondeterminism is an essential feature of distributed systems. Even from the same initial state, different network delays or scheduling decisions may lead to different outcomes.

That nondeterminism gives flexibility, but it also makes correctness harder to guarantee. We need to ensure that the system remains safe under all relevant execution orders, not just a convenient one.

The Difficulty of Consensus

Distributed systems repeatedly face the need for agreement. Multiple nodes must agree on a value, a leader, or an ordering of operations. That turns out to be harder than it first appears.

The FLP impossibility result assumes a completely asynchronous model with no known upper bound on process speed or message delay, deterministic processes, and at most one crash-stop failure. Under those assumptions, no consensus protocol guarantees termination in every admissible execution, even though a message sent to a non-failing process is eventually delivered. FLP does not say that safety and termination are both unachievable in every execution; it limits a deterministic, universal termination guarantee under its stated model.

Practical protocols change those assumptions. Partial synchrony adds timing bounds that hold eventually, failure detectors expose structured suspicions, and randomized algorithms replace deterministic termination with a probabilistic guarantee. An impossibility theorem should therefore be read as a package of computational, failure, communication, and guarantee assumptions, not as a conclusion in isolation.

State Explosion

The state space of a distributed system grows exponentially with the number of nodes. If each of N nodes has K possible local states, then the combined system may have K^N global states.

This state explosion makes it hard to understand all possible behaviors by informal reasoning alone. Formal methods are therefore essential for controlling complexity and guaranteeing critical properties.

TLA+ as an Approach to These Problems

TLA+ (Temporal Logic of Actions) addresses these difficulties through a few key ideas.

• Temporal logic for dynamic properties: properties such as “always” and “eventually” can be written precisely.
• State-transition modeling: a system is abstracted as states and the transitions among them.
• Actions as structured change: state change is described explicitly as an action.
• Fairness assumptions for realistic modeling: the specification can rule out unrealistic executions caused only by pathological scheduling.

TLA+ does not make the essential difficulties of distributed systems disappear. Instead, it makes them explicit and therefore analyzable.

7.2 The Philosophy of TLA+: Actions and Temporal Logic

Leslie Lamport’s Central Insight

One of Leslie Lamport’s most important insights was that system behavior can be understood as a sequence of states. That idea seems simple, but it has major consequences.

Traditional programming often focuses on the execution of commands. Lamport’s view shifts attention from “which instruction ran” to “how the system state changed.” Once that viewpoint is adopted, even complicated distributed behavior can be understood in a uniform way.

A Worldview Based on State-Transition Systems

In TLA+, every system is treated as a state-transition system. The system starts from an initial state and evolves through a sequence of transitions.

【擬似記法】

initial state → state 1 → state 2 → state 3 → ...

The state contains every relevant piece of information about the system: the values of program variables, the status of the network, the local state of each node, and any other information that can influence behavior.

Actions as Abstractions of Change

In TLA+, an action describes a relationship between a current state and a next state. Formally, an action is a predicate over unprimed and primed variables.

For example, an action that increments x can be written as follows.

【擬似記法】

Increment ≜ x' = x + 1

Here x denotes the value in the current state and x' denotes the value in the next state.

The Expressive Power of Temporal Logic

TLA+ uses temporal logic to express dynamic properties of behavior.

TLA+ uses state predicates and actions to describe transitions, then temporal formulas to describe properties of complete behaviors. The basic notation for behavior properties, together with the fairness assumptions used for liveness, is:

• []P (always): P holds in every state;
• <>P (eventually): P holds in some future state;
• P ~> Q (leads-to): whenever P holds, Q eventually follows, an abbreviation for [](P => <>Q); and
• WF_vars(A) / SF_vars(A): weak and strong fairness assumptions for action A.

This book also uses □ / ◇ as mathematical typography, while TLA+ input uses [] / <>.

【Pseudo notation】

[]<>(process = "ready")
<>[](system = "stable")
request ~> response

The first formula says that the process becomes ready infinitely often. The second says that the system eventually reaches a stable condition and stays there. The third says that each state satisfying request is eventually followed by one satisfying response.

Distinguishing LTL Next from TLA+ Prime

The LTL formula X P, often typeset as ○P, evaluates P at the next position of a trace. TLA+ prime notation is different: x' refers to the next-state value of x inside an action, which is a predicate over a pair of states.

Ordinary TLA+ specifications are structured around a stuttering-permitting formula such as Init /\ [][Next]_vars /\ Liveness. This chapter therefore uses actions with primes plus [], <>, ~>, and fairness as its entry points, rather than presenting a next-time operator as a primary TLA+ operator.

The Power of Prime Notation

Prime notation is one of the cleanest ideas in TLA+. It distinguishes the current state from the next state concisely and directly.

【擬似記法】

Transfer ≜
  ∧ amount > 0
  ∧ balance_from ≥ amount
  ∧ balance_from' = balance_from - amount
  ∧ balance_to' = balance_to + amount

This reads naturally as a state change: the amount is positive, the source account has enough funds, and then the two balances are updated accordingly.

The Meaning of Fairness

In a concurrent or distributed system, an action may be enabled forever in the specification and yet never be scheduled in some pathological execution. Fairness is a way to rule out such unrealistic behaviors by assumption. It does not mean that an implementation automatically becomes fair merely because the specification includes fairness.

Here ENABLED A means that from the current state, some next state exists that satisfies action A.

• Weak fairness (WF): if an action is continuously enabled from some point onward, then it cannot be ignored forever. If it remains enabled, it must occur repeatedly.
• Strong fairness (SF): if an action becomes enabled infinitely often, then it cannot be avoided forever. Because this includes intermittent enablement, strong fairness is generally a stronger assumption than weak fairness, although the two can coincide for a particular action and specification.

The following fragment still needs declarations for vars, the actions, Init, and Next, with the fair actions defined as subactions of Next; it is not a complete module that runs on its own.

【Context-dependent snippet】

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

Compositionality

TLA+ supports compositionality. Larger systems can be built from smaller specifications.

【擬似記法】

System ≜ Process1 ∧ Process2 ∧ Process3

Each process can be specified independently, then combined using logical conjunction.

Stepwise Refinement

TLA+ also supports refinement. Development can proceed from an abstract design to a more concrete specification, while the proof obligation runs from the concrete behavior to the abstract behavior it must implement.

【Pseudo notation】

ConcreteSpec => AbstractSpec

The notation above is explanatory rather than an executable TLA+ module. A real refinement proof applies a refinement mapping from abstract variables to expressions over the concrete state and hides internal variables before proving the implication. The mapping and hiding boundary are therefore part of the claim, not incidental implementation details.

Accepting Nondeterminism

TLA+ does not treat nondeterminism as a flaw to be eliminated. Instead, it is a valuable modeling tool. By allowing different actions to be chosen nondeterministically, the specification can preserve implementation freedom while still enforcing the required safety properties.

【擬似記法】

Next ≜ Action1 ∨ Action2 ∨ Action3

The specification does not force one branch to be chosen. Instead, it requires all possible choices to be safe.

Putting Mathematical Foundations to Work

TLA+ is built on set theory, logic, and computation theory, but it integrates those foundations into a notation designed for system engineering. Because it can work naturally with sets, functions, sequences, and quantified formulas, it scales from abstract models to detailed protocol behavior.

Integration with Tools

TLA+ is not just a description language. It is tightly integrated with tooling, most notably TLC, the TLA+ model checker. That integration is one of its most important practical strengths: a mathematically written specification can be checked automatically against concrete finite models.

7.3 State and Action: The Dynamic Model of a System

Structuring the State Space

In TLA+, a state represents the complete relevant information about the system. This may include program variables, network state, local node state, and any other information that affects behavior.

A state can often be understood as a function from variables to values. For example, a banking system might be modeled as follows.

【擬似記法】

State ≜ [
  accounts: [AccountID → Nat],
  transactions: Seq(Transaction),
  current_time: Time,
  network_status: NetworkState
]

This gives a compact description of the full situation at one moment.

Defining Variables and Types

TLA+ makes the state variables explicit, and type-like invariants can restrict them to the values that make sense for the model.

【擬似記法】

VARIABLES
  balance,
  pending,
  log,
  clock

TypeInvariant ≜
  ∧ balance ∈ [AccountID → Nat]
  ∧ pending ∈ SUBSET Transaction
  ∧ log ∈ Seq(LogEntry)
  ∧ clock ∈ Nat

Although TLA+ itself is untyped, such invariants play the role of a type discipline for the model.

Specifying the Initial State

Behavior begins from Init, the predicate describing the initial state.

【擬似記法】

Init ≜
  ∧ balance = [a ∈ AccountID ↦ InitialBalance[a]]
  ∧ pending = {}
  ∧ log = ⟨⟩
  ∧ clock = 0

The initial state fixes what is true at the start of every behavior.

State Change Through Actions

An action describes one way the state can evolve.

Deposit example:

【擬似記法】

Deposit(account, amount) ≜
  ∧ amount > 0
  ∧ account ∈ DOMAIN balance
  ∧ balance' = [balance EXCEPT ![account] = @ + amount]
  ∧ log' = Append(log, [type ↦ "deposit", account ↦ account, amount ↦ amount])
  ∧ clock' = clock + 1
  ∧ UNCHANGED pending

This says that a deposit increases the selected balance, appends a log entry, and advances the clock, while leaving pending unchanged.

The Complexity of a Transfer Operation

Transfers are more complex because several parts of the state must be updated consistently.

【擬似記法】

Transfer(from, to, amount) ≜
  ∧ amount > 0
  ∧ from ≠ to
  ∧ from ∈ DOMAIN balance ∧ to ∈ DOMAIN balance
  ∧ balance[from] ≥ amount
  ∧ balance' = [balance EXCEPT
      ![from] = @ - amount,
      ![to] = @ + amount]
  ∧ log' = Append(log, [type ↦ "transfer", from ↦ from, to ↦ to, amount ↦ amount])
  ∧ clock' = clock + 1
  ∧ UNCHANGED pending

Conditional Actions

Many actions are meaningful only under certain conditions.

【擬似記法】

ProcessPendingTransaction ≜
  ∧ pending ≠ {}
  ∧ ∃ t ∈ pending :
      ∧ CanProcess(t)
      ∧ ExecuteTransaction(t)
      ∧ pending' = pending \ {t}
  ∧ UNCHANGED ⟨balance, log, clock⟩

Nondeterministic Choice

A TLA+ next-state relation often combines many possible actions.

【擬似記法】

Next ≜
  ∨ ∃ account ∈ AccountID, amount ∈ Nat : Deposit(account, amount)
  ∨ ∃ from, to ∈ AccountID, amount ∈ Nat : Transfer(from, to, amount)
  ∨ ProcessPendingTransaction
  ∨ TimeoutCleanup

The system may take any of these actions, provided the chosen action’s constraints are satisfied.

The Importance of Frame Conditions

When an action is written, it is important to make clear which variables do not change. These frame conditions prevent unintended side effects.

【擬似記法】

ReadBalance(account) ≜
  ∧ account ∈ DOMAIN balance
  ∧ UNCHANGED ⟨balance, pending, log, clock⟩

A read-only action should explicitly state that all relevant variables remain unchanged.

Expressing Atomicity

When several changes must happen together, they are written in one action. This is how atomicity is expressed.

【擬似記法】

AtomicSwap(account1, account2) ≜
  ∧ account1 ≠ account2
  ∧ account1 ∈ DOMAIN balance ∧ account2 ∈ DOMAIN balance
  ∧ balance' = [balance EXCEPT
      ![account1] = balance[account2],
      ![account2] = balance[account1]]
  ∧ log' = Append(log, [type ↦ "swap", acc1 ↦ account1, acc2 ↦ account2])
  ∧ clock' = clock + 1
  ∧ UNCHANGED pending

Modeling the Passage of Time

Some systems require explicit representation of time passing.

【擬似記法】

TickClock ≜
  ∧ clock' = clock + 1
  ∧ ProcessTimeouts
  ∧ UNCHANGED ⟨balance, pending⟩

ProcessTimeouts ≜
  log' = [i ∈ DOMAIN log ↦
    IF log[i].timestamp + TIMEOUT ≤ clock'
    THEN [log[i] EXCEPT !.status = "expired"]
    ELSE log[i]]

Interacting with the Environment

A system usually interacts with clients, users, or other external components. That interaction can also be modeled as actions.

【擬似記法】

ReceiveExternalRequest(request) ≜
  ∧ ValidRequest(request)
  ∧ pending' = pending ∪ {request}
  ∧ log' = Append(log, [type ↦ "request_received", request ↦ request])
  ∧ clock' = clock + 1
  ∧ UNCHANGED balance

Modeling Failures

Practical models often need explicit failure actions.

【擬似記法】

NetworkFailure ≜
  ∧ network_status = "operational"
  ∧ network_status' = "failed"
  ∧ pending' = {}
  ∧ UNCHANGED ⟨balance, log, clock⟩

Recovery ≜
  ∧ network_status = "failed"
  ∧ network_status' = "operational"
  ∧ UNCHANGED ⟨balance, pending, log, clock⟩

Constraints as State Predicates

Desired properties can also be written as state predicates and invariants.

【擬似記法】

SafetyInvariant ≜
  ∧ TypeInvariant
  ∧ ∀ a ∈ DOMAIN balance : balance[a] ≥ 0
  ∧ TotalMoney' = TotalMoney

TotalMoney ≜ Sum({balance[a] : a ∈ DOMAIN balance})

This kind of formula captures the consistency properties that every reachable state or transition should respect.

7.4 Temporal Logic: A Language for “When” and “How”

Abstracting Time

Temporal logic is a logical system for reasoning about time. In TLA+, time is abstracted as a sequence of states rather than treated primarily as physical clock time. This makes it possible to describe essential temporal properties without relying on one concrete timestamping scheme.

The power of temporal logic lies in its focus on order and inevitability rather than on precise wall-clock values.

Basic Temporal Operators

TLA+ uses several foundational temporal operators.

□ (always):

【擬似記法】

□P

Example:

【擬似記法】

□(balance ≥ 0)
□(mutex ⟹ ¬(process1_critical ∧ process2_critical))

◇ (eventually):

【擬似記法】

◇P

Example:

【擬似記法】

◇(task_completed)
◇(system_stable)

Combining Operators

Temporal operators can be combined to express richer long-run behavior.

□◇P: P holds infinitely often.

【擬似記法】

□◇(process_scheduled)
□◇(garbage_collection)

◇□P: eventually P becomes permanently true.

【擬似記法】

◇□(leader_elected)
◇□(consensus_reached)

The Leads-To Relation

A very common temporal idea is that whenever A happens, B eventually follows.

【擬似記法】

A ~> B ≜ □(A ⟹ ◇B)

Example:

【擬似記法】

request_sent ~> response_received
failure_detected ~> recovery_initiated

Distinguishing Safety from Liveness

Temporal properties are often divided into two main categories.

Safety: nothing bad ever happens.

【擬似記法】

Safety ≜ □¬BadThing

Examples:

【擬似記法】

□¬(balance < 0)
□¬(deadlock)

Liveness: something good eventually happens.

【擬似記法】

Liveness ≜ ◇GoodThing

Examples:

【擬似記法】

◇(all_processes_terminate)
□(request ⟹ ◇response)

Temporal Expressions of Fairness

Fairness can also be written precisely in temporal form.

Weak fairness:

【擬似記法】

WF_vars(A) ≜ ◇□ENABLED ⟨A⟩_vars ⟹ □◇⟨A⟩_vars

This says that if action A eventually remains enabled forever, it cannot be ignored forever. If it remains enabled, it must occur infinitely often.

Strong fairness:

【擬似記法】

SF_vars(A) ≜ □◇ENABLED ⟨A⟩_vars ⟹ □◇⟨A⟩_vars

This says that if A becomes enabled infinitely often, then it must also occur infinitely often. Since intermittent enablement is enough, this is generally a stronger assumption than weak fairness, although the two can coincide for a particular action and specification.

Note that ⟨A⟩_vars excludes stuttering by requiring that action A occurs and that the tuple vars actually changes.

Temporal Properties of Mutual Exclusion

Mutual exclusion is a standard example of temporal reasoning.

【擬似記法】

MutualExclusion ≜
  ∀ i, j ∈ Processes : i ≠ j ⟹ □¬(pc[i] = "critical" ∧ pc[j] = "critical")

Starvation_Free ≜
  ∀ i ∈ Processes : (pc[i] = "trying") ~> (pc[i] = "critical")

Progress ≜
  (∃ i ∈ Processes : pc[i] = "trying") ⟹ ◇(∃ j ∈ Processes : pc[j] = "critical")

Temporal Properties of Distributed Consensus

Consensus algorithms require several classic temporal properties.

Agreement:

【擬似記法】

Agreement ≜
  ∀ p, q ∈ Nodes :
    (decided[p] ∧ decided[q]) ⟹ (decision[p] = decision[q])

Validity:

【擬似記法】

Validity ≜
  ∀ p ∈ Nodes :
    decided[p] ⟹ decision[p] ∈ {proposed[q] : q ∈ Nodes}

Termination:

【擬似記法】

Termination ≜
  ◇(∀ p ∈ Nodes : decided[p])

Temporal Expressions of Causality

Distributed systems also require temporal reasoning about causal dependence.

【擬似記法】

CausalOrder ≜
  ∀ e1, e2 ∈ Events :
    (e1.timestamp < e2.timestamp ∧ e1.node = e2.node) ⟹
    (e1 happens_before e2)

EventualConsistency ≜
  ◇□(∀ n1, n2 ∈ Nodes : replica[n1] = replica[n2])

Expressing Time Bounds

Practical systems often require bounded-response guarantees.

【擬似記法】

ResponseTime ≜
  ∀ req ∈ Requests :
    (request_sent(req)) ~> (response_received(req) ∧ time ≤ req.timestamp + TIMEOUT)

PeriodicMaintenance ≜
  □◇(maintenance_performed ∧ time_since_last_maintenance ≤ MAINTENANCE_INTERVAL)

Some of these formulas are explanatory and use notation that is not standard raw TLA+ syntax. They should therefore be read as pseudo notation.

Temporal Models of Failure and Recovery

Failures and recoveries are also naturally expressed as temporal requirements.

【擬似記法】

FailureRecovery ≜
  □(failure_detected ~> recovery_initiated)

Availability ≜
  □◇(system_operational)

BoundedDowntime ≜
  □(failure_occurred ⟹ ◇≤MAX_DOWNTIME system_operational)

More Complex Temporal Properties

Real systems usually require several temporal concerns to be combined.

【擬似記法】

SystemSpec ≜
  ∧ Safety_Properties
  ∧ Liveness_Properties
  ∧ Fairness_Assumptions

Safety_Properties ≜
  ∧ MutualExclusion
  ∧ DataConsistency
  ∧ SecurityPolicy

Liveness_Properties ≜
  ∧ Progress
  ∧ EventualTermination
  ∧ ServiceAvailability

Fairness_Assumptions ≜
  ∧ ∀ i ∈ Processes : WF_vars(Step(i))
  ∧ ∀ msg ∈ Messages : SF_vars(Deliver(msg))

The Power and Limits of Temporal Logic

Temporal logic is powerful, but not omnipotent.

It expresses well:

• safety and liveness;
• fairness and progress;
• causal and ordering constraints; and
• recurring or eventual patterns of behavior.

Its limits include:

• quantitative real-time reasoning in full generality;
• probabilistic guarantees;
• explicit resource-consumption analysis; and
• highly detailed numeric optimization.

The key is to choose an abstraction level at which the temporal properties are both meaningful and analyzable.

7.5 Practical Model Checking with TLC

What TLC Is

TLC (the TLA+ model checker) is the principal analysis tool for executable TLA+ specifications. Developed around Leslie Lamport’s work, it explores behaviors of a finite model automatically and checks whether desired properties hold.

The main value of TLC is that it makes mathematical specifications operational. Problems that are hard to spot from formulas alone often appear immediately as concrete counterexamples.

The Basic Principle of Model Checking

Model checking systematically explores the state space of the system and asks whether any reachable state or behavior violates the properties of interest. TLC follows a pattern such as this:

1. generate all states satisfying Init;
2. compute successors using Next;
3. check invariants and temporal properties on the reachable states and behaviors; and
4. report a counterexample trace if a violation is found.

Executability of a Specification

For TLC to analyze a specification, the model must be executable in a finite sense. That means restricting an abstract specification to finite sets and finite bounds that TLC can enumerate.

【擬似記法】

CONSTANTS
  Processes,
  MaxBalance,
  MaxTime

ASSUME
  ∧ Processes ⊆ {"p1", "p2", "p3"}
  ∧ MaxBalance ∈ Nat ∧ MaxBalance ≤ 1000
  ∧ MaxTime ∈ Nat ∧ MaxTime ≤ 100

Creating a Configuration File

TLC is controlled through a configuration file (.cfg) that supplies concrete constant values, the specification to check, and the properties to verify.

【擬似記法】

\* BankingSystem.cfg
CONSTANTS
  Accounts = {"A1", "A2", "A3"}
  InitialBalance = 100

SPECIFICATION Spec

INVARIANTS
  TypeInvariant
  SafetyInvariant

PROPERTIES
  ProgressProperty
  LivenessProperty

A Stepwise Verification Strategy

A staged approach is effective for nontrivial systems.

Stage 1: type-style invariants

【擬似記法】

TypeInvariant ≜
  ∧ balance ∈ [Accounts → Nat]
  ∧ pending ∈ SUBSET Transactions
  ∧ clock ∈ Nat

Stage 2: safety invariants

【擬似記法】

SafetyInvariant ≜
  ∧ ∀ a ∈ Accounts : balance[a] ≤ MaxBalance
  ∧ ∀ t ∈ pending : t.amount > 0
  ∧ TotalMoney = CHOOSE n ∈ Nat : TRUE

Stage 3: liveness properties

【擬似記法】

Progress ≜ □(pending ≠ {} ⟹ ◇(pending = {}))

Controlling the State Space

TLC’s usefulness depends heavily on the size of the explored state space. Good control techniques therefore matter.

Using symmetry:

【Context-dependent snippet】

SYMMETRY Permutations(Accounts)

This is typically used in a model or configuration context to reduce the number of symmetric states that TLC explores.

Adding state constraints:

【擬似記法】

StateConstraint ≜
  ∧ clock ≤ MaxTime
  ∧ ∀ a ∈ Accounts : balance[a] ≤ MaxBalance
  ∧ Cardinality(pending) ≤ MaxPendingTransactions

Analyzing Error Traces

When TLC finds a violation, it reports the execution trace that leads to it. Analyzing that trace is often the fastest route to understanding the root cause.

Typical output example:

【擬似記法】

Error: Invariant SafetyInvariant is violated.

State 1: (Initial state)
balance = (A1 :> 100 @@ A2 :> 100 @@ A3 :> 100)
pending = {}
clock = 0

State 2:
balance = (A1 :> 50 @@ A2 :> 100 @@ A3 :> 100)
pending = {[from |-> "A1", to |-> "A2", amount |-> 50]}
clock = 1

State 3:
balance = (A1 :> 50 @@ A2 :> 150 @@ A3 :> 100)
pending = {}
clock = 2

Detecting Deadlock

TLC can automatically report deadlock when the system reaches a state in which no enabled transition exists.

【擬似記法】

BadMutex ≜
  ∧ pc[1] = "wait" ∧ pc[2] = "wait"
  ∧ ∀ i ∈ {1,2} : UNCHANGED pc[i]

\* TLC may report:
\* Error: Deadlock reached.

Verifying Liveness Properties

Checking liveness is generally more expensive than checking safety. TLC uses specialized graph analysis techniques, such as strongly connected components, to search for liveness violations.

【擬似記法】

EventualProgress ≜
  ∀ i ∈ Processes : □(pc[i] = "trying" ⟹ ◇(pc[i] = "critical"))

A TLC violation report for such a property will typically show a cycle in which a desired event is postponed forever.

Randomized Defect Search with Simulation

For a large state space, TLC model checking may not finish exploring the state graph of the configured finite model. TLC simulation mode instead chooses one enabled successor pseudo-randomly at each step and repeatedly generates behaviors with a bounded length to search for violations and counterexamples. Simulation is neither exhaustive model checking nor probabilistic model checking.

The following CLI example targets TLA+ tools v1.7.4, which is pinned in this repository’s tools/tool-manifest.json (checked on 2026-07-19). Simulation mode itself is selected with -simulate, not by .cfg entries such as CONSTRAINT or COVERAGE; the .cfg file still supplies constants, properties, constraints, and other model settings. Here, num=1000 is the upper bound on the total number of behaviors to generate, and -depth 100 is the maximum number of steps in each behavior. In v1.7.4, file is an absolute-path prefix for generated trace modules, so replace the placeholder with a writable absolute path. Preserve the complete command: -seed supplies the pseudo-random seed, and -aril is the seed adjustment for random simulation. Also preserve the tla2tools.jar version or SHA, the .cfg file, and the termination reason in the execution log.

【Context-dependent snippet】

java -cp tla2tools.jar tlc2.TLC \
  -config BankingSystem.cfg \
  -simulate file=/absolute/path/simulation-trace,num=1000 \
  -depth 100 \
  -seed 20260719 \
  -aril 0 \
  BankingSystem.tla

Finding no counterexample in simulation does not prove the property. Record a result such as simulation-no-violation-observed together with its execution conditions instead of calling the specification “verified.” A guarantee claim requires a separately confirmed completed model-checking run, with its finite model, checked properties, constraints, fairness assumptions, and tool version.

Primary sources are the pinned TLA+ tools v1.7.4 release, the help definitions pinned in the same release’s TLC source for -simulate, -depth, -seed, and -aril, and Lamport’s Specifying Systems. Also check java -cp tla2tools.jar tlc2.TLC -help for the pinned v1.7.4 binary when reproducing the command.

Performance-Optimization Techniques

Several practical techniques improve TLC performance.

Parallel execution:

【Context-dependent snippet】

tlc -workers 8 BankingSystem.tla

Memory tuning:

【Context-dependent snippet】

tlc -Xmx8g -XX:+UseG1GC BankingSystem.tla

Checkpointing:

【Context-dependent snippet】

tlc -checkpoint 60 BankingSystem.tla

Iterative Specification Improvement

In practice, TLC is usually used in an iterative loop.

1. write an initial specification;
2. run TLC;
3. analyze the error or counterexample;
4. improve the specification; and
5. run TLC again.

This cycle gradually improves both the model and the team’s understanding of the system.

Practical Verification Strategy

Useful practical tactics include the following.

• Start small: begin with the smallest model that can express the core problem.
• Expand gradually: add more detail step by step.
• Check continuously: rerun verification when the specification changes.
• Monitor performance: record runtime and state counts to detect scaling issues early.

Understanding the Limits of TLC

TLC also has clear limitations.

• State explosion: the state space can grow exponentially.
• Need for finite models: infinite sets cannot be handled directly.
• Time cost: large models may take a long time to check.
• Memory cost: the number of states is limited by available memory.

Practical use of TLC depends on extracting the maximum value within those constraints.

Executable Example Contracts

The TLA+ fragments in this chapter, especially formulas such as WF_vars(Action) and abstract Next sketches, remain context-dependent snippets unless they are paired with the surrounding VARIABLES, Spec, and configuration file. CI-backed executability is limited to the contract blocks below, which invoke the shared JA/EN canonical assets under examples/** through the manifest runner.

These chapter-level contracts define the pr-quick baseline, while nightly reruns the same canonical assets with deeper exploration settings. Normalized logs, commands, exit codes, stdout, and stderr are expected under .artifacts/manifest/<id>/, and readers should retrieve the examples/** files from the same repository revision instead of copying inline snippets alone.

• tlc-queue-bounded: canonical assets examples/tla/QueueBounded.tla and examples/tla/QueueBounded.cfg; lane pr-quick; pinned version TLC 1.7.4; expected success marker Model checking completed. No error has been found.. Retrieve both the specification and its .cfg from the same repository revision. 【Tool-compliant (runs as-is)】

  node scripts/run-example-manifest.js --id tlc-queue-bounded
  

• apalache-counter: canonical assets examples/apalache/Counter.tla and examples/apalache/Counter.cfg; lane pr-quick; pinned version Apalache 0.52.1; expected success marker Checker reports no error up to computation length 10. Retrieve the whole examples/apalache/ pair from the same commit instead of copying the inline sketch alone. 【Tool-compliant (runs as-is)】

  node scripts/run-example-manifest.js --id apalache-counter
  

7.6 Applying TLA+ to the Real World: A Distributed Consensus Algorithm

The Essence of the Distributed Consensus Problem

Distributed consensus is one of the most fundamental problems in distributed systems. Multiple nodes must agree on a value or decision despite failures, message delay, and uncertainty about the state of the rest of the system.

The challenge is not only to reach agreement, but to do so in a way that keeps the decision stable once made.

A Formal Definition of Consensus

A distributed consensus algorithm is expected to satisfy three standard properties.

• Agreement: any nodes that decide must decide the same value.
• Validity: the chosen value must have been proposed by some node.
• Termination: all non-faulty nodes eventually decide.

In TLA+, we can express them as follows.

【擬似記法】

VARIABLES
  proposed,
  decided,
  decision,
  phase

Agreement ≜
  ∀ p, q ∈ Nodes :
    (decided[p] ∧ decided[q]) ⟹ (decision[p] = decision[q])

Validity ≜
  ∀ p ∈ Nodes :
    decided[p] ⟹ decision[p] ∈ {proposed[q] : q ∈ Nodes}

Termination ≜
  ◇(∀ p ∈ Nodes : decided[p])

Overview of Raft

Raft is a distributed consensus algorithm designed with understandability in mind. It separates the problem into leader election and log replication, which makes the design easier to reason about.

Its central concepts include:

• roles: Leader, Follower, and Candidate;
• terms: monotonically increasing epochs of leadership; and
• log entries: the ordered operations that the cluster agrees on.

The State Model of Raft

A TLA+ model of Raft can make all of these pieces explicit.

【Context-dependent snippet】

VARIABLES
  \* Persistent state on all servers
  currentTerm,
  votedFor,
  log,

  \* Volatile state on all servers
  state,
  commitIndex,

  \* Volatile state on leaders
  nextIndex,
  matchIndex,

  \* Auxiliary state
  messages,
  election_timer,
  heartbeat_timer

Defining the Initial State

Initially, all servers begin as followers.

【擬似記法】

Init ≜
  ∧ currentTerm = [s ∈ Servers ↦ 0]
  ∧ votedFor = [s ∈ Servers ↦ Nil]
  ∧ log = [s ∈ Servers ↦ ⟨⟩]
  ∧ state = [s ∈ Servers ↦ Follower]
  ∧ commitIndex = [s ∈ Servers ↦ 0]
  ∧ nextIndex = [s ∈ Servers ↦ [t ∈ Servers ↦ 1]]
  ∧ matchIndex = [s ∈ Servers ↦ [t ∈ Servers ↦ 0]]
  ∧ messages = {}
  ∧ election_timer = [s ∈ Servers ↦ ElectionTimeout]
  ∧ heartbeat_timer = [s ∈ Servers ↦ HeartbeatInterval]

The Leader-Election Process

Raft leader election can be written in stages.

1. Election timeout:

【擬似記法】

ElectionTimeout(s) ≜
  ∧ state[s] = Follower
  ∧ election_timer[s] = 0
  ∧ state' = [state EXCEPT ![s] = Candidate]
  ∧ currentTerm' = [currentTerm EXCEPT ![s] = @ + 1]
  ∧ votedFor' = [votedFor EXCEPT ![s] = s]
  ∧ SendRequestVoteRequests(s)
  ∧ election_timer' = [election_timer EXCEPT ![s] = ElectionTimeout]
  ∧ UNCHANGED ⟨log, commitIndex, nextIndex, matchIndex, heartbeat_timer⟩

2. Sending vote requests:

【擬似記法】

SendRequestVoteRequests(s) ≜
  messages' = messages ∪
    {[type ↦ "RequestVote",
      term ↦ currentTerm'[s],
      candidateId ↦ s,
      lastLogIndex ↦ Len(log[s]),
      lastLogTerm ↦ IF Len(log[s]) > 0 THEN log[s][Len(log[s])].term ELSE 0,
      dest ↦ t] : t ∈ Servers \ {s}}

3. Processing vote responses:

【擬似記法】

ReceiveRequestVoteResponse(s) ≜
  ∃ m ∈ messages :
    ∧ m.type = "RequestVoteResponse"
    ∧ m.dest = s
    ∧ m.term = currentTerm[s]
    ∧ m.voteGranted = TRUE
    ∧ state[s] = Candidate
    ∧ LET votes ≜ {t ∈ Servers : ∃ msg ∈ messages :
                     msg.type = "RequestVoteResponse" ∧
                     msg.dest = s ∧ msg.voteGranted = TRUE} ∪ {s}
       IN  ∧ Cardinality(votes) > Cardinality(Servers) ÷ 2
           ∧ state' = [state EXCEPT ![s] = Leader]
           ∧ SendHeartbeats(s)
           ∧ UNCHANGED ⟨currentTerm, votedFor, log, commitIndex⟩

Log Replication

Once a leader exists, it accepts client requests and replicates them to the followers as log entries.

1. Appending an entry:

【擬似記法】

AppendEntry(s, entry) ≜
  ∧ state[s] = Leader
  ∧ log' = [log EXCEPT ![s] = Append(@, entry)]
  ∧ SendAppendEntries(s)
  ∧ UNCHANGED ⟨currentTerm, votedFor, state, commitIndex⟩

2. Sending AppendEntries:

【擬似記法】

SendAppendEntries(s) ≜
  messages' = messages ∪
    {[type ↦ "AppendEntries",
      term ↦ currentTerm[s],
      leaderId ↦ s,
      prevLogIndex ↦ nextIndex[s][t] - 1,
      prevLogTerm ↦ IF nextIndex[s][t] > 1
                     THEN log[s][nextIndex[s][t] - 1].term
                     ELSE 0,
      entries ↦ SubSeq(log[s], nextIndex[s][t], Len(log[s])),
      leaderCommit ↦ commitIndex[s],
      dest ↦ t] : t ∈ Servers \ {s}}

3. Processing responses and committing:

【擬似記法】

ProcessAppendEntriesResponse(s) ≜
  ∃ m ∈ messages :
    ∧ m.type = "AppendEntriesResponse"
    ∧ m.dest = s
    ∧ state[s] = Leader
    ∧ m.term = currentTerm[s]
    ∧ IF m.success
       THEN ∧ nextIndex' = [nextIndex EXCEPT ![s][m.source] = m.matchIndex + 1]
            ∧ matchIndex' = [matchIndex EXCEPT ![s][m.source] = m.matchIndex]
            ∧ UpdateCommitIndex(s)
       ELSE ∧ nextIndex' = [nextIndex EXCEPT ![s][m.source] = Max(1, @ - 1)]
            ∧ UNCHANGED matchIndex
    ∧ UNCHANGED ⟨currentTerm, votedFor, log, state, commitIndex⟩

Safety Guarantees

Raft should satisfy several important safety invariants.

【擬似記法】

LogMatching ≜
  ∀ s, t ∈ Servers, i ∈ DOMAIN log[s] ∩ DOMAIN log[t] :
    log[s][i].term = log[t][i].term ⟹
    ∀ j ∈ 1..i : log[s][j] = log[t][j]

LeaderUniqueness ≜
  ∀ s, t ∈ Servers :
    (state[s] = Leader ∧ state[t] = Leader) ⟹
    (s = t ∨ currentTerm[s] ≠ currentTerm[t])

CommittedEntriesNeverChange ≜
  ∀ s ∈ Servers, i ∈ 1..commitIndex[s] :
    □(log[s][i] = log'[s][i])

Incorporating a Failure Model

A realistic distributed-system model must also include failures.

Node failure:

【擬似記法】

NodeFailure(s) ≜
  ∧ state[s] ≠ Failed
  ∧ state' = [state EXCEPT ![s] = Failed]
  ∧ UNCHANGED ⟨currentTerm, votedFor, log, commitIndex,
               nextIndex, matchIndex, messages⟩

Network partition:

【擬似記法】

NetworkPartition ≜
  ∃ partition ⊆ Servers :
    ∧ Cardinality(partition) > 0
    ∧ Cardinality(partition) < Cardinality(Servers)
    ∧ ∀ m ∈ messages :
        (m.source ∈ partition ∧ m.dest ∉ partition) ∨
        (m.source ∉ partition ∧ m.dest ∈ partition) ⟹
        m ∉ messages'

Message loss:

【擬似記法】

MessageLoss ≜
  ∃ m ∈ messages :
    ∧ messages' = messages \ {m}
    ∧ UNCHANGED ⟨currentTerm, votedFor, log, state, commitIndex,
                 nextIndex, matchIndex⟩

Liveness Guarantees

Raft also aims to satisfy progress properties, subject to fairness and network assumptions.

【擬似記法】

EventualLeaderElection ≜
  ◇(∃ s ∈ Servers : state[s] = Leader)

Progress ≜
  □(client_request ⟹ ◇committed)

Fairness ≜
  ∧ ∀ s ∈ Servers : WF_vars(ElectionTimeout(s))
  ∧ ∀ s ∈ Servers : WF_vars(ReceiveMessage(s))
  ∧ ∀ m ∈ MessageType : SF_vars(DeliverMessage(m))

Verifying with TLC

A TLC configuration for a small Raft model might look as follows.

【擬似記法】

\* Raft.cfg
CONSTANTS
  Servers = {"s1", "s2", "s3"}
  ElectionTimeout = 3
  HeartbeatInterval = 1
  MaxLogLength = 5

SPECIFICATION
  Init ∧ □[Next]_vars ∧ Fairness

INVARIANTS
  TypeInvariant
  LogMatching
  LeaderUniqueness
  CommittedEntriesNeverChange

PROPERTIES
  EventualLeaderElection
  Progress

This kind of model lets us search for counterexamples within the configured small cluster, fault scenarios, properties, and fairness assumptions. Even a completed run does not establish correctness of the implementation, omitted failures, or larger configurations.

The broader lesson is that even a complicated protocol such as distributed consensus can have its assumptions and properties written precisely in TLA+ and checked over a finite model with TLC. The resulting evidence should be connected to implementation review, testing, and operational fault handling.

End-of-Chapter Exercises

If you use AI while working through these exercises

• Treat AI output as a proposal; use verifiers to make the final judgment.
• Keep a record of the prompts you used, the generated specifications and invariants, the verification commands and logs (including seed, depth, and scope), and the revision history when counterexamples were found.
• For detailed templates, see Appendix D and Appendix F.

Basic Exercise 1: Understanding Temporal-Logic Notation

Explain the following temporal formulas in plain language and give a concrete example of each in a real system.

1. □(resource_requested ⟹ ◇resource_granted)
2. ◇□(system_stable)
3. □◇(garbage_collection)
4. (critical_section_entered) ~> (critical_section_exited)

For each formula, provide:

• an explanation of its meaning;
• a concrete real-system example; and
• an example of a situation in which the property is violated.

Basic Exercise 2: Describing State and Action

Describe the following system in terms of TLA+ state and actions.

Simple inventory-management system:

• a variable stock stores the current quantity;
• a restock operation increases the quantity;
• a shipment operation decreases the quantity but cannot execute when stock is insufficient; and
• a stocktaking operation corrects the quantity to the accurate value.

Describe:

1. the variable declarations and type invariant;
2. the initial state;
3. the action definition for each operation;
4. the Next predicate; and
5. a basic safety invariant.

Practical Exercise 1: Designing a Mutual-Exclusion Protocol

Write Peterson’s algorithm in TLA+ and verify it with TLC.

Requirements:

• two processes use mutual exclusion;
• each process has the states “noncritical,” “trying,” and “critical”; and
• the protocol is controlled by a flag array and a turn variable.

Properties to verify:

1. mutual exclusion: the two processes are never in the critical section at the same time;
2. progress: if there is a pending request, eventually some process enters the critical section; and
3. fairness: both processes can enter the critical section repeatedly rather than one starving forever.

Practical Exercise 2: The Producer-Consumer Problem

Design a producer-consumer system with a finite buffer in TLA+.

System structure:

• multiple producer processes;
• multiple consumer processes; and
• a shared fixed-size buffer.

Constraints:

• producers must wait when the buffer is full;
• consumers must wait when the buffer is empty; and
• FIFO order must be preserved.

Verification targets:

1. absence of deadlock;
2. no data loss;
3. fairness between producers and consumers; and
4. avoidance of buffer overflow and underflow.

Advanced Exercise: Designing a Distributed System

Design a simplified distributed file system in TLA+.

System requirements:

• multiple storage nodes;
• replication for redundancy;
• client read and write requests; and
• tolerance to node failure.

Main operations:

1. file creation and deletion;
2. file reading and writing;
3. replication management; and
4. failure detection and recovery.

Properties to verify:

1. Consistency: all replicas eventually hold the same contents.
2. Availability: service continues despite some node failures.
3. Durability: data remains persistently stored.
4. Partition tolerance: the system behaves appropriately under network partition.

Design questions:

• How is the failure model defined?
• Which consistency model is chosen: strong consistency or eventual consistency?
• Is distributed consensus required, and if so, which algorithm should be chosen?
• How are performance trade-offs handled?

Through these exercises, you should gain practical skill in formal distributed system design with TLA+. In the advanced exercise in particular, it is important to reason explicitly about the implications of CAP-style constraints and the trade-offs between theory and practice.