Exactly-once is a state machine. Model-check yours.

A review pipeline gives every case two first-level reviews and sends a disputed case to someone else for a second-level review. A small function, the handler, runs on each first-level submit; once both are in and the case is disputed, it sends a second-level assignment (an “L2”) to a queue. It must send exactly one: zero leaves the dispute unsettled, two pays twice. (Read “charge the card” if you prefer.)

Delivery is at least once: a platform that hears nothing back can’t tell a crash from a lost reply, so it resends. AWS Lambda retries a failed asynchronous call (it “attempts to run it two more times” by default), a queue redelivers a message nobody confirmed in time, and two reviews landing together fire the handler twice. So runs of the handler (invocations) overlap, and exactly-once has to be built into it.

The usual fix is a claim: each case has a routing record in the database (the store), and an invocation first does a conditional write (compare-and-set, one atomic step), status ∈ {absent, PENDING} → ROUTING, so of two racers one wins and the other exits as “already routed”. The winner dispatches the L2 and marks the record ROUTED; if the dispatch fails, it resets to PENDING so the retry dispatches again. The tests pass.

It has two bugs. Invocation A claims, then dies before dispatching. Every retry finds ROUTING, fails its claim and exits, so the case is stuck forever. Or A dispatches, the queue accepts the message but replies slowly, and A’s call times out; A resets to PENDING, and the retry, B, claims and dispatches again, creating a second L2.

Each step is correct on its own. Each bug lives in one interleaving (a merge of A’s and B’s steps, or schedule) with a fault at one moment, and with two invocations and up to two faults this handler has 5,629 distinct schedules of up to eight steps. A program can cover them all: write the handler as a state machine (every situation the system can be in, and the steps between them) with invariants that must hold in every reachable state, such as “at most one L2”. A model checker applies every possible step from the start, then from each result, until no new states appear; on a violation it prints the path there, a counterexample or trace.

This post’s checker is about 50 lines of Python. Without faults it finds nothing in all 13 reachable states; with two faults it reaches 141 states and returns both bugs, with shortest traces of two and five steps, in about a millisecond.

In the figure, a railway token instrument, the token is the claim, and a clock that reissues it when the holder doesn’t return is a lease, which cures the stuck case. A holder that was only slow (a garbage-collection pause, say) may wake and keep writing: a zombie. So each claim takes the next value of a counter on the record, the epoch, and the store refuses any write numbered below the highest it has accepted (token #6 bounces once the register reads 7). That number is a fencing token.

The model

A handler is a state machine over the store

A handler that gets exactly-once out of at-least-once delivery is a state machine whose state lives in the store, whose transitions are conditional writes, and whose side effects either happen inside a transition or are idempotent (safe to repeat, usually via an idempotency key the receiver remembers). Writing one down takes three lists.

State is everything that survives a step: the record (status, epoch, whether the lease has run out), the L2 count, and each invocation’s program counter and claimed epoch. A crash erases one program counter and nothing else: the store remembers, the process forgets, and every bug here comes from that asymmetry.

Actions are the steps a process can take (claim, dispatch, mark ROUTED, reset to PENDING), each a function from a state to a next state, plus the environment’s: crash an invocation, fail a call, time out a call that succeeded, pause the lease holder until its lease runs out, redeliver.

Properties are what must hold:

1. At most one L2 per case, a safety property (“nothing bad ever happens”) that a single state can violate.
2. ROUTED is final, since whatever read it already acted on it.
3. Recoverable: from every reachable state, some path still reaches ROUTED. The real goal, “eventually routed”, is a liveness property that needs fairness assumptions to check; recoverable needs none, and it catches the bug that pages people, a state no retry can leave.

The checker is breadth-first search with a visited set, plus a backwards pass for recoverable:

def check(init, actions, invariants, goal=None, limit=2_000_000):
    """Visit every state reachable from `init`, breadth first.

    actions(s) -> [(label, next_state)]; states must be hashable.
    invariants -> {name: predicate}, checked on every reachable state.
    goal       -> predicate for "recoverable": from every reachable
                  state, some path must still reach a goal state.
    BFS order means the first bad state found has a shortest trace.
    """
    parent = {init: None}         # visited set + how we got here
    order, edges, queue = [init], [], deque([init])
    while queue:
        s = queue.popleft()
        for label, t in actions(s):
            edges.append((s, t))
            if t not in parent:
                parent[t] = (s, label)
                order.append(t)
                queue.append(t)
                if len(order) > limit:
                    raise RuntimeError("state space over limit")

    def trace(s):
        steps = []
        while parent[s] is not None:
            s, label = parent[s]
            steps.append(label)
        return steps[::-1]

    out = {"states": len(order), "transitions": len(edges),
           "violations": {}, "bad_states": {}}
    for name, ok in invariants.items():
        bad = [s for s in order if not ok(s)]
        out["bad_states"][name] = len(bad)
        out["violations"][name] = trace(bad[0]) if bad else None
    if goal is not None:
        back = {}                  # reverse edges
        for s, t in edges:
            back.setdefault(t, []).append(s)
        alive = {s for s in order if goal(s)}  # can reach the goal
        todo = list(alive)
        while todo:
            for p in back.get(todo.pop(), ()):
                if p not in alive:
                    alive.add(p)
                    todo.append(p)
        stuck = [s for s in order if s not in alive]
        out["_stuck"] = set(stuck)
        out["bad_states"]["recoverable"] = len(stuck)
        out["violations"]["recoverable"] = (
            trace(stuck[0]) if stuck else None)
    return out

The visited set (parent) expands each state once, because two schedules that reach the same state share its future. The recoverable pass walks backwards from goal states over the explored edges; any state it never marks is a dead end.

The model is the part you write per system: actions(s) returns each enabled step as a label and a next state. The router’s, in check.py, is 65 non-blank lines. Three modelling choices matter most:

• An ambiguous outcome is two actions: a network call worked, failed, or you don’t know. “Times out (was sent)” is the action behind the shortest duplicate, and a mock that only fails before the effect can’t produce it.
• Faults spend a budget (one unit per crash, failed call, timeout, failed status write or pause). That keeps the state space finite and qualifies the result: “holds with up to 2 faults”, not “holds”.
• Redelivery is free and unbounded, so a state stuck here is stuck under any real retry policy.

Reproduce it

Interleavings you can click

The explorer runs a JavaScript port of the same model (a cross-check script asserts it agrees with check.py on state counts and every shortest trace in 40 configurations). It opens on the stuck trace with the recoverable lamp red; play the L2 row for the five-step duplicate, then toggle the fixes. Orange buttons are faults.

idem makes dispatch create-if-absent keyed by case id, lease lets a claim expire and be reclaimed, and fence makes every write after the claim conditional on the claim’s epoch. The checker’s verdict at a budget of 2 faults (a failing cell gives the shortest counterexample’s length):

fixes	states	at most one L2	ROUTED is final	recoverable
none (the design above)	141	fail 5	pass	fail 2
fence	141	fail 5	pass	fail 2
idem	101	pass	pass	fail 2
idem + fence	101	pass	pass	fail 2
lease	485	fail 5	fail 7	pass
lease + fence	405	fail 5	pass	pass
idem + lease	353	pass	fail 7	pass
idem + lease + fence	301	pass	pass	pass

Each fix removes exactly one class of bug: idempotence the duplicates, the lease the dead ends, fencing the zombie.

Fencing without a lease does nothing: the same 141 states and 350 transitions as the original, since without reclaim there is never a second claimant to reject.

A lease without idempotence turns “stuck” into “twice”: A claims, dispatches and pauses past its lease; B reclaims and dispatches again.

A lease without fencing lets a zombie write. The 7-step trace with idem and lease on: A claims (epoch 1) and dispatches; A pauses and its lease expires; B claims (epoch 2); A wakes and marks ROUTED with no epoch check; B’s dispatch fails and B resets to PENDING, so the record goes ROUTED → PENDING. It needs two faults at once: at a budget of 1 fault the checker reports this design as passing all three properties, so tests that inject one failure at a time never see it.

Leases

A lease without a token is a race with a timer

A job-queue worker that drops repeat deliveries by looking for an existing run row has the same shape.

The fix’s WHERE clause is a lease written as a timestamp. Three versions at a budget of 2 faults:

version	states	at most one done write	done is final	recoverable
v0: an existing row means duplicate	17	pass	pass	fail 2
v1: + reclaim of error or stale running	149	fail 5	fail 5	pass
v2: + epoch on the reclaim, checked on every write	113	pass	pass	pass

v0’s two-step dead end is the field note’s bug. v1 answers the open question with yes: A inserts, pauses past its lease, B reclaims, and both “done” writes land. In the other v1 trace, B’s engine error overwrites the done from A’s late write, so the next redelivery runs the job a third time. In the widget, switch the token on and A’s late write, epoch 1 against a row at epoch 2, bounces.

fencing · the same schedule, with and without a tokenjob model, check.py port

fencing token: off replay done writes accepted –

This is Martin Kleppmann’s argument in “How to do distributed locking”, made mechanical: safety “requires the storage server to take an active role in checking tokens, and rejecting any writes on which the token has gone backwards.” Google’s Chubby called the token a sequencer; leases go back to Gray and Cheriton (SOSP 1989).

The model has no clocks: its pause action says only that the lease ran out while A was frozen, so the result holds for every lease and pause length. A longer lease makes the zombie rarer, never impossible. With fencing, the store’s own writes stop depending on timing (effects outside it still need fix 1), and lease length becomes a trade between recovering dead claims fast and fencing out slow live ones.

Batches

The first record votes for everyone

Some bugs in this family aren’t interleavings but a decision made once per batch instead of once per message. Enumeration finds those too.

Routing flags send a record to review; reservedConcurrency = 1 caps the function at one running copy. The widget opens on the field note’s case. Click record 0 to flip it, or switch the gate to per record.

the first record votes for everyone · one batch, two gatesclick a record to flip it

gate records[0] decides per record new batch

has routing flags (must reach review) flag-less –

The batch model in check.py enumerates every batch of up to 3 records (14 complete batches, 29 states). Under the records[0] gate, 4 of the 14 send a flagged record to the default path, the shortest in three steps: enqueue a flag-less record, enqueue a flagged one, process the batch. Routed per record, all 14 pass.

If each record is flag-less with probability q, independently, and a batch holds b records in random order, a flagged record is misrouted exactly when it isn’t at index 0 and the record at index 0 is flag-less:

P(flagged record misrouted) = q · (b − 1) / b

check.py checks the formula against a seeded simulation:

batch size b	flag-less fraction q	q(b−1)/b	simulated
1	any of 0.05, 0.25, 0.5	0	0
2	0.25	0.125	0.1257
10	0.05	0.045	0.0438
10	0.5	0.45	0.4442

At b = 1 the rate is exactly zero, so a suite that sends one message at a time can’t see the bug. In production it scales linearly with q, which somebody else’s deploy controls.

The math

Why enumerate instead of sample

A test matrix enumerates schedules; the checker enumerates states. The original router at 2 faults has 141 states but 5,629 distinct schedules of up to 8 steps, 154,599 of up to 12 and 2,977,545 of up to 16.

For the fully fixed router, states grow with invocations and faults (wall-clock on a laptop from one run of check.py; yours will differ):

invocations	faults	states	transitions	ms
2	1	89	214	0.48
2	2	301	806	1.95
2	3	747	2,244	5.31
3	2	1,049	3,867	8.93
3	3	3,369	13,679	35.11
4	2	3,377	15,748	38.22

Two or three racing invocations and two or three faults cover every bug above, and the search stays under a tenth of a second in pure Python.

The alternative is sampling, as a deterministic simulator does. check.py runs 10,000 seeded random walks of up to 20 steps, choosing uniformly among enabled actions, so faults come up far more often than in any realistic test:

bug	shortest trace	walks that hit it	median steps when hit
original router: stuck after claim	2	72.3%	3
original router: duplicate L2	5	16.72%	10
idem + lease: ROUTED → PENDING	7	4.06%	8
job v1: two done writes	5	7.26%	9
job v1: done → error	5	0.48%	5

Trace length doesn’t predict rarity: the last two rows are the same length, and the second needs two faults in two particular places. Breadth-first search returns every one with its shortest trace, and when it finds nothing, no violation exists in the model within the bound. A random campaign that finds nothing only means you didn’t find anything.

Prior art

Where this sits

TLC, TLA+‘s model checker, is “an explicit-state model checker that can check both safety and liveness properties”, and in breadth-first mode “it will produce a shortest possible behavior that exhibits the error”: ours is a toy version. The experiment folder has the router in TLA+ (Router.tla), and TLC (the rolling v1.8.0 release, build 2026.10.15) reports the same distinct-state count and the same violated safety invariants for all eight fix combinations (141, 141, 485, 405, 101, 101, 353 and 301 states). Recoverable (“from every state, some path”) is a branching-time property, which TLA+‘s linear-time properties don’t express directly, so only the Python checks it. Learn TLA+ is the gentlest route into the real tool.

Newcombe et al., “How Amazon Web Services Uses Formal Methods” (CACM, 2015), applied TLA+ to 10 large systems, including a DynamoDB bug where “the shortest error trace exhibiting the bug included 35 high-level steps.” Nobody writes that test by hand.

A model checker can’t tell you your code matches the model; FoundationDB’s deterministic simulation and Jepsen test the implementation but can’t tell you there is no bad schedule. You want both, and the model costs an afternoon.

Kafka’s exactly-once drops duplicate sends using a producer id and sequence numbers, but the guarantee covers Kafka’s own log: the announcement notes that systems relying on external data stores “support weaker guarantees”, and a dispatch to another queue is outside it. Brandur Leach’s “Implementing Stripe-like Idempotency Keys in Postgres” is the closest prior work to this post’s state machine, down to a “completer” that pushes unfinished requests through.

Fixes

Fixes, ranked

1. Key the effect at the receiver (removes duplicates). Create the L2 as create-if-absent on the case id, so a repeated dispatch is a no-op:

INSERT INTO l2_assignment (case_id, reviewer_pool, created_at)
VALUES ($1, $2, now())
ON CONFLICT (case_id) DO NOTHING;

A transactional outbox is stronger: write the outgoing message in the same transaction as the status change and let a relay publish it. Queue-level dedup is weaker: SQS FIFO drops duplicates only “within the 5-minute deduplication interval”, which a crash retry plus a lease expiry can outlast, and some producers can’t set a dedup id at all.

2. Claim with a lease and an epoch, and fence every later write (removes dead ends and zombies).

-- claim or reclaim: returns a row only if this caller won
UPDATE routing
   SET status = 'ROUTING', epoch = epoch + 1, owner = $2,
       lease_until = now() + interval '5 minutes'
 WHERE case_id = $1
   AND (status = 'PENDING'
        OR (status = 'ROUTING' AND lease_until < now()))
RETURNING epoch;
-- (plus INSERT ... ON CONFLICT DO NOTHING for the "absent" case)

-- every write after the claim
UPDATE routing SET status = 'ROUTED'
 WHERE case_id = $1 AND status = 'ROUTING' AND epoch = $my_epoch;
-- 0 rows updated: you are a zombie. Stop, and do not retry.

Use the store’s clock for lease_until, so skew between machines’ clocks doesn’t move the deadline. In a key-value store the same check is a condition expression on status and epoch.

3. Make something come back. With two retries, a claim whose holder crashed is reclaimable but may never be reclaimed. A sweeper that re-triggers rows WHERE status = 'ROUTING' AND lease_until < now() (Brandur’s completer) turns “recoverable” into “recovered”.

4. Route per record, or reject mixed batches (removes the batch class). If the batch API forces one decision, partition the batch by route first and report per-record failures.

5. Write concurrency assumptions down as tests (mitigates). If correctness depends on a single writer, add a test that reads the deployed concurrency setting from your infrastructure code and fails if it changes. Better, move the state into the store and delete the assumption.

Detect it

Monitors are invariants with a pager

Each property in the model is also a query you can alarm on:

• One effect per key: SELECT case_id FROM l2_assignment GROUP BY case_id HAVING count(*) > 1 returns nothing. If the receiver is keyed, count dispatch attempts per case instead; a rising number is a retry storm.
• Nothing stuck: alarm on any row WHERE status = 'ROUTING' AND lease_until < now() - interval '10 minutes' (without leases, use the claim time). In the original design this is the only signal that the stuck state exists.
• Terminal stays terminal: reject or log any write that moves a row out of ROUTED or done, with a trigger or the write’s own condition.
• Counts are conserved: second-level count ≤ first-level count per run.

Then turn each counterexample into a regression test: drive the real handler through the trace’s steps, with hooks where the test injects each fault the model has. With fakes for your own store and queue:

def test_timeout_after_send_is_not_a_second_l2(store, queue):
    # the trace's fault: "dispatch → times out (was sent)"
    queue.fail_next_send(after_enqueue=True)
    try:
        handle("c1", store, queue)   # A: claim, send, then timeout
    except TimeoutError:
        pass                         # the invoker will retry
    handle("c1", store, queue)       # B: the retry
    assert queue.assignments_for("c1") == 1

Keep the model next to the handler, run it in CI, and change both in the same pull request.

Try it

Try it

Everything above comes from the scripts in experiments/exactly-once-is-a-state-machine/:

# every model and table in this post; writes results.json
python3 -I check.py
# the widgets' JS port vs results.json, 40 configurations
node crosscheck.mjs
# Router.tla under TLC, all 8 fix combinations (needs Java)
TLA2TOOLS=./tla2tools.jar sh tlc.sh

To check your own handler, copy check() and write actions() for your states. Start with the claim, give every network call three outcomes, add a crash after every step that writes, make redelivery free, and set the fault budget to 2. If your design survives, raise the budget and add an invocation.