kill9 - your agent survived the crash. Did the money?

An agent transfers $100. The tool call goes out, the bank commits it, and the process dies before the result reaches durable state. Kubernetes restarts it. The agent reloads its checkpoint, sees a transfer it never finished, and calls the API again.

Two transfers, one authorization.

Testing this means killing the process at exactly the wrong moment, and the wrong moment is a different instant in every run. kill9 finds those moments and kills there on purpose.

• What it is. A deterministic crash-recovery tester for AI agent harnesses. It kills an agent process in the gaps between model intent, human approval, external side effects, durable persistence, and model observation.
• What it does. It doesn't sample random crash points. It discovers a run's semantic boundaries by observing it, kills at each one - or at an ordered schedule of controller decisions - and judges what comes back against four contracts.
• The result that surprised me. Pointed at an ordinary LangGraph application, not one contract could be decided. Not "the app failed" - the question could not be asked at all. That became the finding, and the rest of the project measures what it costs to fix.
• Get it. docker compose up -d && python -m kill9.cli check examples/transfer_agent - about two minutes to a red result, on a clean clone. github.com/egehazar/kill9.

A real run at 14× speed. The clock reports true elapsed time.

The failure class

Durable execution frameworks promise that a crashed workflow resumes correctly, and they deliver that for workflow state - the graph knows which node it was in. What they can't promise is that the outside world and the agent's beliefs about the outside world stay consistent with each other across the crash.

Four things go wrong independently. They are the four contracts:

contract	the question it asks
action continuity	was one authorized action performed once, or did recovery turn it into two?
authority integrity	did every effect carry a human approval bound to that specific action?
knowledge truthfulness	is what the agent believes and says about the world actually true?
conversation integrity	is each result bound to the request it answers, exactly once?

Authority integrity is the one that only breaks under a crash. A human approves a transfer, and the approval is durably recorded - as a resume value at a position in the graph. The process dies. On restart, the checkpoint faithfully records that something was approved at that point, and nothing records what. The agent proceeds on an approval that no longer refers to anything.

That is the default red result from the command above: third boundary of a five-node graph, about two minutes.

Why not random crashes

Chaos-monkey sampling fails here for two reasons.

The dangerous windows are narrow. The gap between "the bank committed" and "we wrote that down" is milliseconds inside a run that takes seconds, so uniform sampling spends nearly all its budget killing an idle process. And a random hit isn't reproducible, so you can't tell whether your fix worked - a bug you can't reproduce is an anecdote, not a finding.

So the harness announces its own semantic boundaries as it runs: before dispatch, after the world commits, when persistence lands, when the result reaches the model. The controller kills at each announced boundary in turn. The five-node demo graph announces 41 of them. Crash testing stops being a lottery and becomes an enumeration in which every cell has an address you can replay.

Two consequences shaped everything after.

A defect has a shape. Its failing set isn't scattered - it occupies a specific, reproducible region of the boundary sequence. Identity defects live in an interval, open at dispatch and closed when the result becomes durable. A lie written to durable state occupies a suffix, because once persisted, every later cut inherits it. A correlation defect isn't positional at all: it fails 42/42 or 0/42 depending only on which concurrent stream goes first, because recovery regenerates it.

A run is a schedule, not an event. Once the controller can address a boundary, it can hold a thread there, release it, kill at a second point, and restart - an ordered program of decisions. That turned out to be load-bearing rather than decorative.

Four verdicts, not two

A PASS/FAIL checker lies, and always in the same direction.

The checker asks whether every dispatch carried a bound approval, and looks for durable dispatch records. There are none, because the application never wrote any. The predicate quantifies over an empty set, holds vacuously, and the contract reports PASS - the strongest verdict available, emitted exactly when the checker knows least.

So verdicts are four-valued:

• PASS - the property was checked and held.
• FAIL - the property was checked and was violated.
• INCONCLUSIVE - the evidence is present but doesn't settle it.
• UNOBSERVABLE - the question could not be asked. Not a pass, not a failure. The system did not record what the property is about.

Plus one thing that isn't a verdict: EXPERIMENT_INVALID. If a barrier never armed or a world gate didn't hold, the cell is discarded. A defect in the instrument never becomes a finding against the target. It has fired on my own bugs more often than I'd like, which is the point of having it.

The vacuity guard went in after the first version shipped. I pre-registered the expected impact, then verified differentially across 1,167 cells: zero verdicts changed except the vacuous ones. A correct fix moves exactly what it claimed it would and nothing else.

Ground truth from outside the system under test

Asking the agent's own logs whether the transfer happened twice is asking the suspect for an alibi. Three independent evidence streams:

• W - the world. A separate FastAPI + SQLite ledger, the only authority on what happened externally. It commits before it responds, so a crash between commit and response is a real lost acknowledgement rather than a simulated one.
• H - the harness. The agent's durable state, read back through LangGraph's own serde, plus an observing checkpointer that announces persistence boundaries.
• M - the model. A scripted model server, so the agent's reasoning is deterministic and the same crash produces the same run every time.

Determinism is what makes a certificate possible. A failure gets a fingerprint and a YAML file, and kill9 replay <cert> re-executes the schedule and re-derives the verdict from artifacts alone. All nine committed certificates replay. A crash finding nobody can reproduce on demand is worth very little to whoever has to fix it.

The main finding: an ordinary agent app can't be checked at all

Everything above ran against my own target, with defects I planted. A tool that only finds bugs its author planted has proven nothing.

So I wrote a second application: an idiomatic LangGraph support agent - create_react_agent + ToolNode + PostgresSaver, human-in-the-loop through the prebuilt interrupt path, no kill9 concepts anywhere in it. The kind of thing you get by following the framework's own tutorial.

Every contract returned UNOBSERVABLE, at every crash point.

The application isn't wrong. It persists exactly what LangGraph persists, which is a faithful record of graph state. It does not record which logical action a tool call belongs to, whether a dispatch was attempted, what the human approved, or what the model was told afterward - because nothing asks it to. Without those, "did recovery turn one action into two?" has no answer in durable state.

The easy misreading is that kill9 only works on applications built for it. The real claim is stronger and holds regardless of the checker: recovery correctness is not decidable from durable state alone in the ordinary case, because ordinary applications don't record the things these properties quantify over.

What it costs to fix

A negative result that stops there is a complaint. So I measured the observability floor - the minimum an application must persist before each contract becomes decidable - by adding instrumentation one increment at a time and re-running the entire matrix at each level.

level	what it adds	what becomes decidable
L0	nothing - the idiomatic app	-
L1	world calls carry a run-scoped id	-
L2	+ a durable action row per tool call, with an idempotency key	action continuity, authority integrity
L3	+ a durable approval row bound to that action	-
L4	+ a durable record of what the model is about to be told	knowledge truthfulness
L5	+ the exposure announced as it's handed to the model	conversation integrity

The pre-registration predicted the first necessary increment would be the durable action row. It was wrong, and wrong downward: beneath it sits a run-scoped id on world-facing calls. Without one you can't attribute an effect to a run at all, so it sits beneath every contract rather than one. The whole table is five short diffs - a logging discipline, not a rewrite.

Three more results

Human decisions survive recovery. Two concurrent tool calls, each with its own human review, the operator accepting one and rejecting the other, killed at all 30 boundaries the flow announces. 29 cells judged, and the rejection landed on the right call in every one - including the cell where the crash lands before the proposals are durable, the model regenerates both with entirely new call ids, and the rejection still tracks the right one.

The region has documented history: LangGraph #6533 (resume values misrouted between tools in a ToolNode) and #6626 (parallel interrupt() calls generating identical ids) describe this class of failure. Both are closed, and both are about steady state. Whether the correlation survives a crash is a different question, and neither issue asks it. On langgraph==1.2.6, it does.

Failure geometries compose as a product. Across 71 two-crash schedules, failing sets compose as a plain disjunction over epochs, with no interaction term - but shape doesn't compose that way at all. An interval crossed with a suffix produces neither: it produces a two-coordinate object, one per epoch, each keeping its own geometry. I had pre-registered the first half and not the second.

Every detector has now detected. An unexercised predicate is indistinguishable from a broken one. Across 1,211 committed cells, eight of the sixteen predicates had never returned FAIL on real evidence - implemented, unit-tested, shipping in certificates, and never once shown to fire on the defect they exist to catch. Eight seeded defects later, each the smallest thing that trips exactly one predicate and each verified to fire alone against a clean control, all sixteen are confirmed detectors.

Two things I got wrong

An address that was complete and still didn't decide. I believed a crash site was fully specified by a boundary plus the frontier - the announced-but- unreleased barriers at the moment of the kill. Twelve repetitions at one boundary gave PASS ×11, FAIL ×1, with a byte-identical frontier every time. A frontier enumerates blocked barriers, and the thread whose progress actually decided the verdict was running free between them, so it appeared in no frontier at all.

That is why schedules exist: hold the deciding thread at its own barrier first, then kill at the original point. FAIL ×12, race gone. The frontier describes a crash site; a schedule constructs one. Two repetitions agreeing - what my earlier gate checked - is not evidence of determinism. It's two samples of a biased coin agreeing.

An observer that couldn't observe. The first parallel-interrupt sweep reported decision fidelity broken in all 29 cells, which would have been the most serious thing I'd found. It was false. The component that decodes durable state wrote to a path whose parent directory didn't exist, the caller's check=False swallowed the error, and the reader saw "no checkpoints decoded" - indistinguishable from "the application persisted nothing."

A silent non-observation, in the one component whose entire job is to observe, producing a dramatic false positive. Dramatic results are the ones you are least motivated to re-check. An undecodable cell now returns an explicit decoded: false and is excluded rather than counted as a failure, and a separate scorer recomputes the whole result from committed artifacts as an independent check.

Limitations

• Every violation kill9 found on its own target is one I planted. The unseeded findings are about the instrument - the coin-flip address, the vacuous PASS, the silent decoder - plus one measured negative. A deliberate hunt on an unseeded application found nothing, and that is recorded as a negative result rather than dropped.
• Exploration is bounded, never exhaustive, with bounds declared per run and recorded in every artifact. Reduction is shape-preserving, not mechanism-preserving: a two-crash shape isn't reachable with one crash and the reducer correctly refuses to shrink it, but a one-crash witness for the same underlying bug can still exist.
• One framework, one topology, two concurrent calls. Everything here is one adapter deep.
• Where a framework's prebuilt interface can't express a correlation, I record it as an interface gap - distinct from a framework correctness defect and from an application defect. Collapsing those three would be unfair to the framework and useless to the reader.

What I'd build next

Streaming, deferred with the reason recorded: token output leaves the checkpoint boundary, and the knowledge contract's questions change shape once the model has already said something the system never persisted. Three or more concurrent interrupts, and rejecting the first rather than the second. And a second framework - deciding whether these are properties of durable agents or properties of LangGraph needs a second data point.

Where everything lives

The tool, the four contracts and sixteen predicates, all nine replayable certificates, the observability floor, the full evidence tree, and an 18-entry design-review log of every belief a run falsified are at github.com/egehazar/kill9.