Formal modeling for distributed systems correctness with TLA+ and PlusCal
Learn states, actions, invariants, safety, liveness, TLA+, PlusCal, TLC counterexamples, epoch fencing, and refinement through one protocol.
The whole story in 16 lines
Model the contract above code, explore every small interleaving, repair the counterexample, and then connect the proof obligation back...
- A useful property translates a broad promise into safety and liveness obligations.
- A state is one complete assignment of relevant values, not a log line or a server.
- An action describes every legal before-and-after change without choosing an implementation.
- A behavior is a sequence of complete states produced by repeatedly taking allowed actions.
- A safety failure has a finite bad prefix that shows exactly where the promise broke.
- A liveness claim needs explicit fairness assumptions because eventually is about whole behaviors.
- An inductive invariant starts true and remains true after every allowed action.
- Abstraction removes details only when they cannot change the property being checked.
- Dropping a correctness-bearing variable can merge distinct cases and make the property impossible to state.
- Nondeterminism lets the checker explore every relevant event ordering instead of one lucky run.
- Failures belong in the model as possible actions, not as surprising exceptions.
- PlusCal actor steps translate into TLA+ actions over a compact shared state.
- TLC explores reachable states, deduplicates repeats, and reports a trace to a violation.
- A counterexample is a concrete execution that turns a vague suspicion into a design problem.
- Epoch fencing rejects work from an authority that has already been replaced.
- Model evidence is strongest when refinement and fault testing connect the abstraction to real code.
Setup
Ava and Ben are both trying to reserve seat 42, the final seat, while leadership moves from R1 to R2. The dangerous object is an old commit from R1 that remains in the network after R1 stops.
To reason about that message, we need two simple handles. A state freezes every fact that matters at one moment, while an action says which complete state may legally follow it.
Two owners would break safety because that outcome must never occur. A request that waits forever would break liveness, even if no duplicate owner ever appears. One protocol can fail in either way.
PlusCal will let us write the actors and their atomic moves precisely. TLC will then choose among those moves in every small ordering we allow, including the delayed commit a normal test may miss.
The notation can wait. Our first problem is more basic: “one seat, one owner” sounds clear to people, but a checker needs to know exactly which snapshots and executions that promise forbids.
Promise
The troubling execution gives us a plain product promise: only one client gets seat 42, and a healthy request eventually receives an answer. Both halves matter, but they make claims about different shapes of evidence.
“Only one” forbids a snapshot containing Ava and Ben as owners, regardless of message order or leader. “Eventually” rules out an endless execution where a healthy request keeps waiting despite enough opportunities to finish.
Words such as healthy and eventually rely on shared intuition, while a checker has none. Which part can one bad snapshot refute, and which part requires us to inspect what keeps happening over time?
The promise separates cleanly. Safety rejects any state with a forbidden outcome, while liveness rejects behaviors that withhold progress forever under the assumptions we choose. The checker must therefore search for two different kinds of failure.
Switch Contract among Safety, Liveness, and Both. Compare whether a single forbidden snapshot, an endless non-progressing behavior, or both evidence shapes are needed to refute the promise.
We can now say what the service owes without choosing its code. To recognize two owners in one state, the checker next needs a precise definition of one complete moment across disagreeing servers and in-flight messages.
State
The state strip gathers every fact needed to judge seat 42 at one mathematical moment. It is not any server’s private view. It is the model’s complete assignment for epoch, leader, pending work, and owner.
More replicas do not automatically require more kinds of variables. Three servers may hold different local views, yet epoch and leader identify authority while pending work and ownership determine whether the promise still holds.
Server logs remain useful evidence, but an in-flight commit may appear in none of them at the instant we care about. Can the newest-looking log alone define the complete state of this distributed protocol?
One state now means the whole assignment: epoch 7, leader R1, both requests pending, and no committed owner. Those values describe one distributed moment even though no single machine has to store that exact record.
Freezing the system gives us a precise noun, but a protocol also needs verbs. We must say which complete assignment may follow this one, especially when the delayed epoch-7 message arrives during epoch 8.
Actions
An action relates the complete state before a move to the complete state after it. That relation describes legality above the code level, so several implementations can realize the same Elect, Prepare, or Commit rule.
Elect changes leader and epoch together. Prepare records pending work without creating an owner. Commit is separate because turning a request into ownership is exactly where stale authority can damage the contract.
R1 created a well-formed commit during epoch 7, but it reaches the gate after R2 starts epoch 8. Should valid bytes from an old authority still define a legal Commit transition?
The earlier execution stays fixed while the Commit relation changes. An unfenced rule adds Ava beside Ben. A fenced rule compares epochs and records a rejection, so its after-state preserves one owner.
Toggle Fence off and on. Follow the same delayed epoch-7 commit as it either adds a second owner or becomes rejected work in the complete after-state.
A fence looks promising, but one before-and-after pair cannot establish the whole design. Distributed systems create long chains of legal actions, and correctness must survive every chain the model permits.
Behaviors
One legal action gives us two adjacent snapshots. Repeating that choice produces a behavior: a sequence of complete states that records how every modeled fact changes through one possible execution.
The same starting state can grow several behaviors because Ava and Ben may prepare, retry, or commit in different orders. The model does not bless one timeline as the way the network behaves.
A test captures the schedule that happened on one machine under one load, and that evidence still matters. What about the other legal schedules that different delays, retries, or leader changes can produce?
Ava-first and Ben-first are different behaviors from the same model. Their middle states and final owner can differ, so our correctness claim cannot quietly depend on whichever ordering a test happened to observe.
Switch Schedule between Ava first and Ben first. Keep the initial state fixed and compare how the ordering changes the final owner of seat 42.
We now face a large family of behaviors rather than one story. Fortunately, a safety claim has a sharp failure shape: one finite path ending in a forbidden state is enough to disprove it.
Safety
The behavior tree turns alternative schedules into finite branches. Safety says that none of those branches may reach a forbidden state, so the checker can stop as soon as the first red leaf appears.
For seat 42, uniqueness forbids two owners. Current authority requires every accepted commit to carry the live epoch. Durability can separately require storage to finish before the service acknowledges success.
Elections, prepares, and delays can all remain legal until one transition changes the decisive value. Which final action turns the old epoch-7 message from an awkward possibility into a finite safety counterexample?
Different last actions create different red leaves: duplicate ownership, stale authority, or acknowledgment before durability. Each leaf supplies the exact finite prefix that broke a named rule, not a general fear about concurrency.
Switch Bug among Duplicate, Stale epoch, and Torn write. Compare which final state refutes uniqueness, current authority, or durable-before-acknowledgment.
Safety can reject one bad snapshot, but it cannot object to a system that takes no useful action forever. That frozen protocol has no red leaf and still fails every waiting client.
Liveness
Ava’s waiting request gives us the missing question. Liveness asks whether it eventually completes across the rest of a behavior, which no single snapshot can answer by itself.
The scheduler can keep choosing unrelated work while every state remains safe. Ava then waits forever without producing a forbidden snapshot, so progress requires an explicit assumption about when enabled work receives a turn.
Suppose Commit becomes enabled in recurring windows but never stays enabled continuously. Which fairness assumption prevents starvation without demanding that every temporary opportunity run immediately?
No fairness permits endless starvation. Weak fairness helps when Commit stays enabled continuously. Strong fairness also covers infinitely recurring opportunities, so the assumption changes which infinite behaviors the specification accepts.
Switch Fairness among None, Weak, and Strong. Compare whether Ava can starve, must finish under continuous enablement, or must also finish across recurring windows.
Fairness makes the progress claim honest by naming what the environment must eventually allow. For safety, we need a different shortcut: one rule that every reachable state inherits from Init and Next.
Invariants
For the safety half of our contract, the candidate invariant says that seat 42 has at most one committed owner. We want that predicate to travel with every reachable state, not just the examples already drawn.
The first gate is Init. Every allowed starting state must already satisfy the rule, because no argument about future actions can repair an invalid state that the model permits at the beginning.
Init only establishes the starting point. If an arbitrary state satisfies the invariant and then takes any allowed Next action, what must be true of the resulting state?
An inductive invariant passes both gates: Init establishes it, and every possible Next action preserves it. The same argument can test uniqueness, current authority, or durable-before-acknowledgment across all reachable states.
Switch Rule among Unique owner, Current epoch, and Durable first. See which candidate survives both induction gates and where an action breaks the others.
Induction extends one local preservation argument across an unbounded chain of reachable states. TLC still needs a finite model to explore, so we must remove production detail without removing the cause of our bug.
Abstraction
The induction argument does not need thread-pool sizes, byte encodings, metric names, and every storage callback. Keeping them would multiply states while adding nothing to the ownership question.
Epoch, leader, pending messages, durability, and owner survive the projection because changing any one can change whether seat 42 is correct. Abstraction is selective forgetting for a specific purpose.
Smaller models explore faster, which makes aggressive simplification tempting. If the projection removes epoch, can it still distinguish a commit from the current leader from the same commit under stale authority?
The useful abstraction is not the smallest possible state. It is the smallest state that preserves every distinction capable of changing the property, including the boundary between epoch 7 and epoch 8.
Switch Abstraction among Too detailed, Useful, and Too coarse. See whether extra noise hides the bug or removing epoch erases it.
Calling an abstraction useful is still a claim we should test. Our stale and current commit cases differ only in epoch, so the next experiment removes that one variable and follows the information loss.
Projection loss
The two concrete records differ only in their epoch relationship: one is stale and one is current. Select the EPOCH token to remove that fact, then follow both records as the projection collapses them into one checker state that cannot answer the authority question.
Interleavings
Restoring epoch gives the checker its lost distinction back. It still does not choose which enabled message arrives next, because choosing for the network would hide the race we are trying to judge.
Ava’s and Ben’s deliveries are both ready in this state. Either may become the next action, so the fork admits that the environment, not our test harness, owns the order.
A familiar test run may always deliver Ben first and look reassuring. What must the model do with Ava first and with the retries or leader changes that can grow from it?
Keeping both arrows means one source state yields two concrete schedules. The rules stay fixed while the intermediate states and final owner can change, so neither branch can stand in for the other.
Switch Delivery among Ava first, Ben first, and Explore both. Follow who can own seat 42 when the model refuses to choose a favorite order.
The order is now honestly open. But our old epoch-7 commit still needs to survive long enough to meet epoch 8, so the network model must explain what delay, loss, duplication, and crashes actually do to messages.
Failures
Opening the schedule is not enough if every message arrives promptly and every server stays alive. The counterexample needs the network to retain Ava’s epoch-7 commit while leadership moves on.
A delay leaves bytes in flight, a drop removes that delivery and enables retry, duplication creates another delivery, and a crash stops R1’s future actions. None of them automatically erases a message that already left R1.
R1 has crashed, R2 leads epoch 8, and Ava’s old commit remains in the network. Which modeled fault can make that stale work arrive after Ben commits?
Delay supplies the missing physics. It holds the epoch-7 commit across the election and later releases ordinary bytes into an epoch-8 system, while drop, duplicate, and crash produce different enabled actions.
Switch Fault among Delay, Drop, Duplicate, and Crash. Watch the path and enabled actions change, especially whether the old commit can still reach storage.
We have named the actors, state, legal moves, scheduler choices, and failure physics. The design is precise enough to write, but loose pseudocode could still change what one atomic move means.
PlusCal + TLA+
PlusCal gives each participant a lane for exactly those moves: R1 prepares and sends, R2 is elected and commits, and the network decides when delivery occurs. The shared strip still holds the state we have been reasoning about.
A label marks one atomic step. At that boundary the process reads the before-state, applies its updates, and advances its program counter, so one implementation-shaped block cannot hide several model actions.
The lanes look algorithmic, yet TLC does not execute PlusCal as production code. What mathematical object must these labeled actor steps become before a checker can enumerate behaviors?
Translation produces Init plus a Next relation whose alternatives are the enabled labeled steps. The readable actor story and the state-machine semantics now describe the same choices from two useful viewpoints.
That translation is the handoff, not a deployment artifact. With a finite set of clients, epochs, and seats, TLC can start at Init and follow every enabled Next action instead of watching one script run.
TLC
TLC begins with every assignment allowed by Init. For each node it applies every enabled Next action, builds the successor assignments, and checks the invariant before expanding again.
Different histories sometimes reach the same epoch, pending set, and owner. TLC merges those histories at one state key because identical current assignments have identical modeled futures.
Elections, retries, commits, and delayed deliveries widen the frontier quickly. Does the unique-owner invariant survive every reachable branch, or does one branch finally admit Ava beside Ben?
At depth three a red node becomes reachable. The graph still reconnects duplicate assignments, so the finite search spends its work on distinct states while preserving every path needed to explain the violation.
Adjust Depth from two through four. Find the first depth where the delayed-commit sequence can reach the red uniqueness state.
Within these chosen values and bounds, this is exhaustive search rather than a lucky sample. The red node is useful because TLC can now return the exact choices that led there.
Counterexample
TLC turns the red node into a counterexample trace: a row of complete states joined by the one action selected at each transition. We can read it as the shortest bug story the model found.
R1 prepares Ava in epoch 7 and sends a commit that the network delays. R2 then takes epoch 8, prepares Ben, and commits him while Ava’s old bytes remain in flight.
Ben now owns seat 42 and the invariant still holds. Which last enabled action converts the stale message from leftover work into a second owner?
The final Commit accepts Ava’s epoch-7 message beside Ben’s epoch-8 result. The trace pins the failure to one transition: storage trusted a well-formed message without checking whether its authority was still current.
That is narrower than saying failover is risky and far more actionable. We can replay this exact trace, keep every earlier choice fixed, and change only the commit boundary that accepted stale authority.
Fence repair
★ If you remember one thing · An epoch fence turns the same delayed stale commit from a second success into a rejection.
The repair comparison starts from the same counterexample on both sides. Elections, preparations, Ben’s commit, and Ava’s delay are identical. Only the rule at the storage boundary changes.
When Ava’s epoch-7 message arrives, the unfenced side asks only whether the commit is structurally valid. The fenced side also compares its carried epoch with the current epoch 8.
One equality check looks almost trivial next to the whole protocol. Can it really change the outcome of this otherwise identical execution?
Yes. The unfenced path records Ava beside Ben, while the fenced path rejects epoch 7 and leaves Ben as the single owner. A local boundary rule restores the global uniqueness invariant for this trace.
Switch Fence between Fenced and Unfenced. Keep the delayed message fixed and watch it become either rejected stale work or a second owner.
The abstract repair is clear: authority must travel with the work and be revalidated where the work takes effect. The remaining question is whether the real service implements that same action boundary.
Evidence
A passing repaired model says something precise about the specification, not automatically about the deployed service. The code may serialize epochs differently, split Commit across calls, or contain a failure the model never named.
A refinement mapping connects those concrete events back to abstract actions: this database write is Commit, this term is epoch, and this internal retry is a stuttering step that leaves abstract state unchanged.
Even a careful mapping can omit a code path or environmental assumption. What evidence can press on the implementation where the small model deliberately stops?
Fault tests provide the complementary lane. Model checking explores every bounded abstract behavior, while implementation tests inject delays, crashes, and retries through real code. Their overlap is stronger than either lane alone.
Switch Evidence among Model, Fault test, and Both. Compare which gap remains when behavior-space coverage or implementation reality stands alone.
Our conclusion is deliberately conditional: the contract held within the model’s finite bounds, fairness assumptions, and refinement mapping. Those named boundaries tell reviewers exactly what production tests and further models still owe.
Recap
With that evidence boundary visible, retrace the investigation from the question that started it. We split one winner and an eventual answer into safety and liveness because a forbidden state and endless waiting require different evidence.
Those obligations forced us to define one moment precisely. A state became the full assignment of epoch, leader, pending work, durability, and owner, including facts no single server log could hold.
Once the moment was complete, the next problem was change. Actions related before-state to after-state and made Commit’s authority check a protocol rule rather than an accident of one implementation.
Chaining actions gave us behaviors, not just isolated transitions. The same initial assignment could grow Ava-first or Ben-first schedules, so one observed test run could never define correctness.
Across those branches, safety had a compact witness: any finite prefix ending with two owners disproved uniqueness. That let the checker stop at the exact transition that created the red state.
But an execution could avoid every red state by doing nothing useful forever. Liveness therefore looked across an infinite behavior and became honest only after we named fairness for enabled work.
For safety, induction supplied the shortcut. Init had to establish the candidate invariant, and every Next action had to preserve it, carrying one local predicate across all reachable states.
That reachability search made state size matter. We removed threads, encodings, and metrics while keeping epoch, ownership, and every other distinction that could change the answer.
The projection counterfactual tested that boundary instead of trusting it. Dropping epoch merged stale and current authority into one abstract state, proving that a smaller model can also lose its question.
After restoring epoch, nondeterminism kept both enabled deliveries open. The model did not guess the network’s favorite schedule. It admitted every order allowed by the state.
Failure actions then gave the old commit somewhere to live. Delay kept epoch-7 bytes in flight across R1’s crash and R2’s election instead of treating failover as magical message cleanup.
With actors and physics fixed, PlusCal expressed their atomic steps in readable lanes. Translation turned those labels into Init and Next without changing the state-machine choices we meant to check.
TLC expanded that finite transition system, merged repeated assignments, and checked the invariant at every reachable node. At depth three, one distinct branch finally turned red.
The returned trace made the branch legible: prepare Ava in epoch 7, elect R2, commit Ben in epoch 8, then accept Ava’s delayed commit. Timing suspicion became a reproducible design error.
Replaying the same trace with epoch fencing isolated the repair. The identical old message was rejected at the commit boundary, so one local authority check prevented a second global owner.
Finally, refinement mapping and fault tests carried that abstract rule toward production while keeping assumptions visible. Given every tool we used, what one question holds the whole method together?
The method asks whether every behavior allowed by the specification satisfies the contract under the assumptions we stated. A counterexample identifies the broken rule, while a bounded pass identifies the evidence we earned and where more evidence is still needed.
The whole story in 16 lines
Model the contract above code, explore every small interleaving, repair the counterexample, and then connect the proof obligation back...
- A useful property translates a broad promise into safety and liveness obligations.
- A state is one complete assignment of relevant values, not a log line or a server.
- An action describes every legal before-and-after change without choosing an implementation.
- A behavior is a sequence of complete states produced by repeatedly taking allowed actions.
- A safety failure has a finite bad prefix that shows exactly where the promise broke.
- A liveness claim needs explicit fairness assumptions because eventually is about whole behaviors.
- An inductive invariant starts true and remains true after every allowed action.
- Abstraction removes details only when they cannot change the property being checked.
- Dropping a correctness-bearing variable can merge distinct cases and make the property impossible to state.
- Nondeterminism lets the checker explore every relevant event ordering instead of one lucky run.
- Failures belong in the model as possible actions, not as surprising exceptions.
- PlusCal actor steps translate into TLA+ actions over a compact shared state.
- TLC explores reachable states, deduplicates repeats, and reports a trace to a violation.
- A counterexample is a concrete execution that turns a vague suspicion into a design problem.
- Epoch fencing rejects work from an authority that has already been replaced.
- Model evidence is strongest when refinement and fault testing connect the abstraction to real code.