Verifying software
when agents write
most of it.

An agent will produce a plausible implementation of nearly anything you describe, and it will produce a plausible implementation of the wrong thing with the same confidence. When one person wrote every line, reading scaled with output at roughly one to one, so review effort took care of itself. That relationship does not hold any more. More change can land in an afternoon than I can responsibly read in a week, and the useful question moves from whether the code looks right to which mechanical checks stand between a mistake and the person it would land on.

There is a boundary worth naming before the rest of it, because everything below sits inside it. Every check compares an implementation against something that was already written down. None of them can tell you the written-down thing was the right thing to want. That gap does not close with better tooling, and it is the reason the practices are arranged the way they are: the machinery takes the parts that can be settled by running something, and a person keeps the parts that cannot.

• CharterName the harms, before there is code to sweep. Who can be hurt by this system, and what their worst day looks like. The ranking is a person’s and it goes on the record.
• Still earlyReplay whatever has already gone wrong. Past incidents are the least speculative evidence available. An incident that maps to no entry means the list is missing one.
• Once code existsMap the seams. Where the durable writes are, where outside data becomes trusted inside data, and which concepts are defined in more than one place.
• Per harmWork out what would actually catch it. Ten questions that turn an intent into a property something can check, and that force the answer “nothing, yet” to be written down when it is the true one.
• StandingKeep a record of the checks that exist. What each one settles, and what it cannot. Consulted before a review starts rather than after.
• Each batchSay which harms this batch of work is allowed to move. Named up front, and the coverage notes get updated in the same change as the code that moved them.
• After it landsReview cold. Someone with no shared context checks what landed against the brief, not against the builder’s account of it.
• Before effectsWalk the control structure. Before a path that can spend, send, publish or delete goes in — where can control fail while every component does exactly what it was built to do.
• Every incidentAsk which harm this was. The first artifact of an incident is that answer, and the property that would have caught it. The fix comes after.

The loss ledger

A per-project list of the unacceptable outcomes in a person’s world, ranked worst first, with what stands in front of each one and an honest section for what nothing stands in front of. Entries are written as harm rather than as failing components, so that someone who has never seen the codebase can still argue with the ranking. Turning the list over this way is what makes a gap visible: enumerate the harms first and an uncovered one becomes a line with a blank beside it, where an inventory of checks would simply never have grown the row. It is a list maintained by the same machinery it exists to keep honest. Its authority comes from a person ruling on the entries, and from its coverage lines pointing at checks that genuinely run.

Oracle selection

An oracle is whatever tells you a run was correct. Ten questions turn a fuzzy intent into one: the first five generate candidates by asking what must never happen, what is conserved, what two independent things must agree, how the output has to move when the input is transformed, and what round-trips. Two more decide where the property is asserted and which kind of error is affordable there. The last three are an honesty pass — make the check fail on purpose, write down what it cannot see, and write down what is being taken on faith. Placement is easy to get wrong in a way that looks fine. A property stated upstream of the point where being wrong becomes harm can pass by construction while the failure it was written for sails through underneath.

The deciders inventory

A live record of the mechanical checks a given project actually has wired up, and for each one, the question it settles next to the question it does not. The rule attached to it is that a review names the decider it will reach before it starts. Where there is no decider, the brief says so, and the output is then read as judgement rather than as evidence. An inventory tracks what got built, so it can never tell you what you are exposed to. That is the ledger’s job, and the two are kept as separate views of one set of facts.

Seam maps

Three inventories of the code, kept on disk rather than in a conversation: every durable write and what authorises it, every point where untyped or external data becomes trusted internal data, and every domain concept defined in more than one place. They are what makes the rest of it concrete, because a harm is much easier to argue about once you can point at the exact places that could cause it. They go stale quietly as the tree drifts. The sweep is expensive, so the date of the last one is recorded and the staleness is meant to be visible rather than discovered.

Hazard analysis

Nancy Leveson’s STPA, from Engineering a Safer World (2011). Instead of hunting for bugs it draws the control structure — who commands what, who is told what came back — and walks every control action against a fixed set of ways control fails: not given when needed, given when it should not be, given too early or too late, stopped too soon or held too long. It finds the states where a system hurts someone while every component does exactly what it was specified to do, which is a category ordinary code review is not shaped to catch. Completeness is bounded entirely by the diagram, and the bound is silent. It also says nothing about how likely anything is; that judgement has to be added separately.

Cold review

A reviewer with no shared context with whoever built the thing, checking what landed against the brief rather than against the builder’s report of it. Evidence gets ranked rather than pooled: a mechanical check first, then observation of the real system, then a differential comparison, then a reviewer conditioned differently, and a second reviewer of the same kind as the weakest thing on the list. Agreement between reviewers is evidence and not certification. Knight and Leveson showed in 1986 that independently built versions fail together far more than independence predicts, and two agents drawn from the same few underlying models have no obvious claim to more independence than two engineers taught from the same textbook. Nothing in the loop checks the brief, so a review can pass against a wrong brief and be working exactly as designed.

Property-based testing

Rather than choosing example inputs, state the rule that should hold for all of them and let a generator go looking for the case that breaks it. It is the cheapest way to get real coverage of the input space, and it tends to find the inputs nobody would think to write down by hand. An intermittent red under a generator is often a real ordering or timing defect rather than flake — but not reliably, and telling the two apart takes an investigation. The practice earns its keep where an intermittent failure gets that investigation instead of a re-run.

Model checking, occasionally

For a small and carefully bounded path, write the model as a state machine and enumerate every reachable state rather than testing a sample of them. It is worth the trouble in one narrow situation: a concurrent or replayed path where the code has run ahead of any written specification and the interesting failures are orderings rather than values. Used here on a confirmation path, where it settled questions that had stayed open through review and turned up a defect nobody had written down. It decides things about the model, not about the code. A model that omits the mechanism carrying the bug will happily report that the bug cannot happen.

Traceability — tried once

The idea is borrowed from avionics practice under DO-178C: trace forward from each requirement to the code and the check that covers it, and backward from each piece of code to the requirement or the harm that justifies it. Anything that traces to nothing is either dead code or evidence the requirements are incomplete. Historically this was expensive human labour, which is the part agents plausibly change. Run here once so far. The run was seeded with a planted defect to prove it could find anything at all — it did — and the real candidates it surfaced are still being ruled on. An orphan it finds is real; a run that finds none proves very little.

The same split gets set per project, and on client work it is written down before anything starts — how agents are handled on your code →

A check is sound if it never passes wrong behaviour, and complete if it never flags correct behaviour. No check is generally both, so the useful move is to decide which pole a given one is being built toward and then read its result accordingly. A gate is built sound for one named property, which makes its pass mean something you can act on. A hunter is built wide to go looking for trouble, which makes its failure meaningful and its silence close to uninformative.

Most of the trouble I have seen comes from one confusion between those: a hunter running clean gets quoted as though something had been certified. A static analysis pass that finds nothing is worth having, and so is a fuzzing run that did not crash. Neither is a pass in the sense a gate produces one, and reading either as though it were is how a project ends up holding a clean report over a path nothing was actually watching.

There is a quieter version of the same error, and it is the one that caught me. A check can exist, be correct, be current in the tree, and still not have run in the session someone is holding up as proof. A test sitting in a suite that needs a database the default command never starts is invisible to the command everyone actually types, and a coverage claim read in good faith calls it covered. The fix was to make each coverage claim name the suite its test belongs to, so a tool can ask the honest question: was that suite reported on at all, and did this test inside it actually execute. An unobserved check is a worse state than a failing one, because a failure at least tells you something moved.

Everything here checks an implementation against something already written down, so the specification itself stays unchecked. If the brief was wrong, a green run means the wrong thing was built accurately, and every practice above will report success. That is the residual, it is structural, and the honest response is to keep a person answerable for the brief rather than to add another layer of machinery underneath it.

Two smaller limits worth stating plainly. Coverage percentage and mutation score make poor targets: the first mostly tracks how large a test suite is, and the second is only informative in its particulars — which mutants survived, and under which guard — not as a number to govern by. And adding a second agent to look at the first agent’s work buys much less than it appears to, because two models conditioned the same way tend to be wrong in the same places; a differently built check is worth more than another opinion.

This is a working practice rather than a finished framework, and parts of it are younger than others. Where something has not been tried yet, this page says so.