Your agent is a distributed system. Check it like one.

2026-09

Not every agent failure is the LLM's — and the other kind is the one you can find before production does. Here's the case, on the confirmation button almost every serious agent has: the race, the fifty-line spec that finds it, the rule that falls out, and the six shapes the same bug takes.

Every team that ships an agent eventually has the same conversation. Something went wrong — a duplicate refund, a batch of tickets created twice, an approval that seemed to apply to the wrong thing — and the first question in the room is “what did the LLM do?” Sometimes the LLM did something. More often, in my experience, the LLM did exactly what it should have, and the system around it did something no one had thought to check.

I want to make the case that agent reliability has two halves, that most of the effort goes into one of them, and that the other half is easier than it looks — because it isn’t new. An agent that has a second process, a retry, or a human in the loop is a distributed system. Everything we know about distributed systems applies, including the tools for proving what they guarantee.

Two kinds of nondeterminism

An agent system has three parts, and only one of them is an LLM.

The LLM decides. The runtime carries state between decisions — memory, history, checkpoints, pending approvals — and moves effects into the world. The world has its own state and its own failure modes.

Failures in the LLM’s decisions are LLM nondeterminism: sampling, prompt sensitivity, a wrong tool picked. It’s irreducible. You manage it statistically, with evals, judges and thresholds, and you should.

Failures in how the runtime carries state and effects are system nondeterminism: which of two concurrent turns wins, what a retry does, what a crash leaves behind, which version of state a component read. This kind is reducible in a way the first is not. Bound it — two turns, one retry — and for a given design the set of possible interleavings is finite. A model checker, a tool such as TLC that explores every interleaving a design allows, can enumerate all of it. Those tools are decades old and well understood.

The two kinds aren’t in competition. Both can cost you money, and both need handling. My claim is narrower: the second kind gets much less attention than the first, and it can be fixed independently of the LLM. The failures in this post are all of that kind — in each of them, the LLM’s decisions were the intended ones.

What “reliable” can actually mean

Three different guarantees hide behind that word, and they cost very different amounts.

Most teams have the first and wish for the third. This post is about the second: the cheap middle, and the only tier that answers the question an incident actually raises — can this happen again? You don’t make the agent deterministic. You make the runtime’s guarantees definite: written down, and shown to hold under every interleaving, no matter what the LLM emits. The LLM becomes an adversary in your proof rather than a collaborator. That idea is old too: a monitor around an untrusted component can enforce any safety property, whatever the component decides to do.

Here’s what that looks like on one protocol.

A worked example: the confirmation button

Take the one almost every serious agent has.

Our platform is the usual shape: an orchestrator reads the user’s message, picks a domain agent — tickets, finance, HR, a dozen others — and delegates. Domain agents call tools. Anything risky (creating a batch of tickets, bulk-completing or deleting them, posting a journal entry) stops and shows a confirmation card. The user clicks, or types “go ahead”, and the next turn picks up where the last one stopped.

We had just rewritten this to be rigorous. A confirmation now produces a pending action record: exact operation, targets, parameters, and a fingerprint of the world at the time it was shown. Approval binds to that record. Spending it writes a receipt — the durable record that stops a “yes” from being reused. If you’ve built a confirmation step, you’ve built some version of this. It reads as obviously correct.

I read the diff the way you read any large PR these days — five or six thousand files, most of them written by a coding agent — function by function. Everything did what it said. None of it answered the only question that mattered: could a “yes” ever be used twice? That answer isn’t in any function. It’s in how two turns, a retry and a crash interleave, and nobody holds that in their head across thousands of files. Reading was never going to settle it.

That is the shape of question model checkers are for. I wrote the promise down as a TLA+ spec and let TLC look for a counterexample, expecting a corner case or two around the crash window. It came back with seven steps and no crash in them. A user clicks once, twenty-four tickets appear — and the part that stung was that the LLM had done everything right along the way.

The race is a textbook one. A turn restores the approval from history, claims it in memory, calls the tool, and writes the receipt only after the tool returns. Two turns — a click and a typed “go ahead” a second apart:

Check, then act, with the record updated last. Anyone who reads between the check and the write sees an unspent approval. No crash, no retry, no LLM error — a read racing a delayed write.

The lost update hiding in “resume”

The repair most teams reach for — record the spend before acting, and re-read the durable record at the check — is not enough, and the checker shows why in nine steps. Both turns read the record and see unspent. Both claim. Turn 1 writes spent and executes. Turn 2 writes spent — it already was — and executes anyway.

That’s a lost update — two readers see the same value, both write — the textbook read-modify-write race. It’s easy to miss when the words are turns and receipts rather than readers and writers; the agent vocabulary hides the shape.

The rule, once you see it, fits in one line:

Spend the approval atomically, spend it before you act, and never resume from a view older than the last spend.

Unpacked, that’s three conditions. An approval can be used at most once only if all three hold, and dropping any one of them produces an interleaving that executes twice — each a failure with an old name:

1. The spend is atomic. “Check it’s unspent” and “mark it spent” happen as one step — a compare-and-set on the record — or else only one turn at a time is allowed to try. Without it: the lost update above. Two turns check, both see unspent, both mark, both execute.
2. The spend comes before the effect. The record says spent before the tool is called, not after it returns. Without it: a resurrected approval. The effect runs first, the record is updated afterwards, and a turn that restores in between sees an unspent approval.
3. Resumes see the latest spend. A turn that restores an approval reads a view at least as fresh as the most recent spend. Without it: a stale view. The spend was written, but the restoring turn is looking at a snapshot taken before it.

Those three conditions are the whole protocol, and fifty lines of TLA+ can check them. Strip out everything product-specific and parameterise by the three choices a team actually makes — when the spend is recorded, whether the check re-reads the durable record, whether turns are serialised.

New to TLA+? A spec is a list of actions; each one says when it may happen and what changes. A plain name is a value now; a primed name like log' is the value after the step. /\ is and, \/ is or, == is is defined as. Four variables here: pc[t] is turn t’s stage, log is the durable record (unspent or spent), view[t] is what turn t read when it started, and eff counts effects in the world. If you already read TLA+, skip this.

\* What a turn sees when it checks: the live record, or the snapshot it started with.
Sees(t) == IF FreshView \/ SpendMode = "cas" THEN log ELSE view[t]

\* A turn may claim the approval when it is ready and sees the record as unspent.
\* With a compare-and-set ("cas"), the same step also marks the record spent.
Check(t) == pc[t] = "ready" /\ Sees(t) = "unspent"
            /\ ~(Serialize /\ Busy)              \* if serialised: one turn at a time
            /\ pc' = [pc EXCEPT ![t] = "claimed"] \* this turn's stage becomes "claimed"
            /\ log' = IF SpendMode = "cas" THEN "spent" ELSE log

\* Calling the tool: one more effect in the world.
Effect(t) == pc[t] = (IF SpendMode = "before" THEN "armed" ELSE "claimed")
             /\ eff' = eff + 1

\* The two properties, checked in every reachable state.
AtMostOnce     == eff <= 1                       \* never two effects
NoResurrection == (eff >= 1) => (log = "spent")  \* once it ran, the record says so

This is an excerpt: the UNCHANGED clauses every TLA+ action needs, plus the restore, spend and record steps, are left out so the argument is visible. The complete, runnable spec is fifty lines and linked at the end of this post.

Here is what that buys you. Each row below is a way a team might implement the spend. For each one, the checker tries every interleaving of two turns and answers the question the review couldn’t — can the action run twice? — and its quieter cousin: can the record still say unspent after the action ran? Where the answer is yes, it hands back the shortest interleaving. A couple of seconds per row.

Two things in that table are hard to get any other way. Every No is a proof, not a passing test: every interleaving of two turns was enumerated, so there is none left for production to discover. And every Yes comes with the exact interleaving that breaks the property, which is the regression test you write next. Code reading gives you neither. Testing gives you the second only when you get lucky with timing.

Each failing row is missing at least one of the three conditions. Recording the spend after the effect breaks spend before you act: for a window the record says unspent about an action that ran, and a turn that restores inside that window runs it again. Re-reading the record but writing it in a separate step breaks spend atomically — that’s the lost update. The two designs that pass, compare-and-set and one-turn-at-a-time, are the two ways of making the spend atomic, and both record it before the effect.

It also explains the near misses. An idempotency key at the backend bounds the effect count but not the authority count — your audit trail still says a spent approval is unspent. Recording the approval before executing the tool (which some SDKs get right architecturally) is necessary but not sufficient without an atomic, durable spend and a fresh view.

You might assume your framework handles this. Read its docs as an interface contract and you’ll find it says the opposite, politely. One documents that on resume the runtime “restarts the entire node from the beginning” and that “any code that ran before the interrupt will execute again.” Another states that any code before the wait “must be safe to repeat.” A third tells you your resume handler “should be idempotent for safety.” The MCP maintainers, in the accepted Tasks proposal, agreed that “a dedicated proposal should introduce a general mechanism for message idempotency across the protocol.” Even Temporal, which exists to make execution durable, documents that Activities “may be executed more than once” and recommends an idempotency key built from the workflow run and activity IDs. None of this is a scandal. It’s a contract most agent teams have never read as one.

It isn’t one bug: six shapes

Once you’ve seen one of these, the rest name themselves. The same handful of failure modes show up in every agent product. Each has a name older than the field, and each is ruled out by a property you can write down.

Two things to notice. Every row is about state and time, not about intelligence. And every “old name” has a known fix that has been in production somewhere for decades. Agent stacks reimplement these protocols per product, usually inside the chat transcript, with an LLM in the decision path — and so they rediscover the bugs one incident at a time.

The dropped-surface row is the one reading would not have found. Two facts about our platform were each written down in a different reviewer’s notes: events are routed to the conversation’s newest connection, and the history keeps only the first final answer per connection. Nobody had put them together. Together they mean that when two turns overlap, the second turn’s confirmation card is silently dropped while the system believes it was shown. The checker composed them in a ten-step trace; a test against the real code reproduced it. Reading finds facts; it does not compose them across components.

The approval protocol is just the first place to look. The same skeleton is under the rest of the stack:

• Memory compaction. Does the summary preserve every fact a later step depends on? That’s refinement — the compacted state still has to implement the full one.
• Multi-agent handoff. Can two sub-agents hold the same capability at once? That’s mutual exclusion over a lease.
• Tool retries. Does at-least-once delivery compose with a non-idempotent effect? That’s exactly-once, and the answer is usually no.
• Streaming and delivery. Is what the user saw what the system recorded? That’s the dropped-surface row, and it fails exactly the way ours did.

How to check your own agent

The goal is not “formally verify the agent.” It’s to get invariant-tier answers for the two or three protocols where the irreversible actions live — approvals, resume, retries — and to make those answers part of the workflow rather than a one-off. Here are the four steps, with the tool, the objective and the deliverable at each.

Step 0 — Write the promise. (30 minutes, a table in the design doc.) Pick one protocol. Write three to seven properties as single sentences, each citing where the promise is made: the design doc, the PR description, the product copy. Write down the gaps the design already admits, too — a crash window, a retry, a path with no record. Those are allowed behaviour, and listing them stops you from finding them again later as bugs. This table is the contract. Everything below checks against it, and reviewers read the PR against it instead of against their own mental model. Write it from the docs and the product promise, not from the code: a contract derived from the code can only confirm what the code does.

Step 1 — Property tests against the real code. (One to two days.) Tools: Hypothesis’s RuleBasedStateMachine in Python, fast-check model-based testing in TypeScript. The rules are your protocol’s actions — restore, claim, spend, execute, retry, crash, deliver the same message twice. The invariants are the properties from step 0. Fake exactly three things: the backend or tool transport (so it can count effects), the LLM (scripted decisions), and the client connections. Keep the real code for restore, claim, spend and dispatch — that’s the part under test. Done when every property has a test and the tests run in CI on any PR that touches the protocol. Expect this step alone to catch the resurrected-approval and stale-view shapes; it caught both of ours.

Step 2 — Model check the design. (One to two days the first time, hours after that.) Tools: TLA+ with the TLC model checker; Alloy if your question is about structure rather than ordering. Write the protocol’s actions at the granularity of your code’s awaits and commits, the same properties as invariants, and small constants — two turns, one approval, at most one crash. Model the runtime’s state transitions, never the LLM’s reasoning: the LLM is a nondeterministic choice at each decision point, and the spec has to hold for every choice. If you can, have someone other than the author of step 0 do this, from the code alone. Our first pass built the model from reviewers’ notes, and the checker faithfully rediscovered everything in the notes and nothing else. Keep the spec under a hundred lines; if it’s growing past that, you’re modelling too much. Done when TLC explores every state with no error, or hands you a counterexample — which you then turn into a step-1 test. This is also where you ask design questions you can’t ask code: add each candidate fix as a switch and let the checker tell you which combination is minimal.

Step 3 — Keep it alive. (Ongoing, minutes.) The contract lives in the design doc. The property tests live in CI. The spec lives next to the design doc and re-runs in seconds when the protocol changes. Add one line to the PR template: does this touch a spend, restore or effect path, and which property covers it? The reviewer’s job becomes checking the promise, not re-deriving the interleavings from the diff.

Where it fits in a week:

Do step 0 before the code exists if you can. We did it at review time — the last cheap moment — and it still paid for itself.

For the design review itself, a checklist:

• The spend of an approval is a compare-and-set, or restores are serialised per conversation.
• The spend is durable before the tool call, not after it returns.
• Every restore reads a view at least as new as the last spend.
• The executed action equals the approved one — operation, targets, and parameters.
• What the user was shown is persisted before they can act on it.
• An effect that happened is always disclosed, especially on the error path.

If your agent passes all of that, you have something most agent products don’t: a reason to believe the confirmation button means what it says.

Objections

Isn’t this just idempotency keys? Partly, and you should use them. But an idempotency key bounds effects at the backend. It doesn’t tell your runtime that an approval was spent, so the next turn still restores it, still claims it, and your audit trail still says it’s unspent. You need both: the backend dedups effects, the runtime spends authority atomically.

Doesn’t durable execution solve this? It moves the problem to a place with better primitives, which is progress. It doesn’t remove it. Durable execution is at-least-once by default, and its own docs tell you to make effects idempotent yourself. Adopting it means you’ve admitted you’re building a distributed system — which is the right admission.

Do I need TLA+, or can I just write tests? Start with tests. A stateful property test that drives your real resume path with a fake backend catches most of the six shapes above. Reach for a model checker when the bug depends on an interleaving you can’t make a test generate on purpose, or when you want the negative result — “no single fix suffices” — that testing can’t give you.

Isn’t the interesting nondeterminism the LLM’s? For product quality, yes. For whether an approved action can run twice, no — and no amount of sampling answers that question.

Try it

The complete spec, the five configurations from the table and the script that runs them are at github.com/jinyuanlu/tla-agent-approval. You need Java and one jar; each row takes a couple of seconds. To check your own design, copy a .cfg, set SpendMode, FreshView and Serialize to what your code does, and run TLC on it — when a property fails, the log holds the interleaving that breaks it, step by step. The same two properties, as a stateful property test against your real code, are in the README.

Why now

Formal methods were expensive for a long time, and the expense was never the checker — TLC has been free for decades. It was the writing: getting a spec out of a design doc and a codebase, and keeping it honest as the code moved. That is the part that has changed.

The specs behind this post were written the same way the code was: a coding agent did the transcription — reading the design doc and turning promises into properties, reading the code and turning await points into transitions — while I decided what to model and what to leave out. The counterexamples and the tests that replay them: the same division of labour. What used to take a week of an expert’s attention now takes a day, and the day is spent on judgement rather than typing.

That reverses the usual objection. If generated code is close to free, then producing it is no longer the bottleneck; knowing whether it is right is. A reviewer who cannot read five thousand generated files needs a way to check the promise instead of the diff. So the skills worth building now sit one level above unit tests: writing down what must hold, property-based testing, deterministic simulation, and model checking. TLA+ for protocols. P if your system is a set of asynchronous state machines. Lean if you need proofs. Whichever you pick, the goal is the same — catch the design error before the code exists, because the code is now the cheap part.

We had never had formal methods in our pipeline. We do now: the contract table, the property tests and the spec are part of design review for the approval path, and the PR template asks which property covers a change. Not because the team became formalists, but because the cost dropped below the cost of the incident.

Further reading: Jane Street on formal methods and the future of programming — the same argument from a shop that has run this way for years; Antithesis on deterministic simulation testing, the replayable tier from earlier in this post; and the P language, which AWS uses to model its distributed systems.

The spec, the five configurations and the runner, with the results table reproduced: github.com/jinyuanlu/tla-agent-approval. Next: the same properties against the open frameworks, version by version, and the table that comes out.