The verification problem

The first time we raced an encoding of Belgium's social-security contributions against EUROMOD, the two disagreed. Our version computed roughly €20.9 billion in employee and employer contributions across a simulated population of workers; EUROMOD, the European Union's reference tax-benefit model, came out €643 higher.

Was that €643 a success or a failure?

The number alone cannot tell you, and the reason it cannot is the reason this chapter exists. Six hundred forty-three euros is consistent with a dozen different underlying realities. It could be floating-point dust—hundreds of thousands of rounding differences, each a fraction of a cent, smeared across the population and piling up into something that looks like money. It could be a single catastrophic error: one worker whose contributions the encoding got wrong by €643 while every other record matched to the euro. It could be a small systematic bias, a rule applied a hair too generously to everyone. Or it could be the worst case of all, the one that looks best from a distance: large errors in opposite directions—tens of thousands of euros too high in one place, tens of thousands too low in another—canceling almost perfectly on their way to a reassuring total.

An earlier chapter watched that last failure mode play out in the wild. When CBO scored the Affordable Care Act in 2010, its projection of the total uninsured rate landed within a percentage point of what actually happened—while getting the composition badly wrong, overstating exchange enrollment by more than half and understating Medicaid by nearly as much, the two errors partly canceling on the way to a roughly-right aggregate. The total was approximately right for the wrong reasons. If your only test is whether two totals are close, you cannot distinguish a model that is right from a model that is wrong in a flattering way.

So we did not compare totals. We compared workers. For each of the 78,479 simulated workers, we lined up the encoding's contribution against EUROMOD's and took the difference. The largest single-worker discrepancy in the entire population was three cents a year. Not three cents on average—three cents at the very worst. Every one of the 78,479 workers matched the reference model to within the width of a rounding error, and the €643 in the aggregate turned out to be exactly what it looked like once we refused to look at it from far away.

Aggregate agreement can hide anything. Per-unit comparison hides nothing.

That sentence is the whole chapter, and it is the answer to the question that hangs over everything agents now build: how do you trust law encoded by a machine? You don't. Trust is the wrong frame. You verify, one unit at a time, against something that is true independently of the machine—and you wire the verification so tightly into the pipeline that an encoding which fails it cannot ship. Verification is not a quality-assurance step bolted onto the method. It is the method. An encoding no one has checked against ground truth, at the level of the individual determination, is not a cheaper version of a validated model. It is confident fiction with good production values.

The ladder of checks

Before an encoding is ever raced against another model, it has to survive a more basic demand: every number in it must come from somewhere. In the pipeline we built at the Axiom Foundation ,^[1] the first gate is one we call the money-atom check, and it is merge-blocking. Every monetary obligation in an encoding—each rate, threshold, taper, and cap that actually moves money—must be grounded in a quoted excerpt from the governing source: the statute, the regulation, the agency manual, quoted verbatim with a pointer to where it lives. An amount with no provision behind it does not get flagged for a reviewer to consider later. It fails the build, the way a syntax error fails the build. When we finished the Belgian encoding, it carried 539 distinct monetary obligations, and the gate demanded a source excerpt for every one of them; the count of ungrounded obligations was zero. The interesting part is not that it reached zero. It is that the gate is configured so the count can only ever fall.

Grounding is necessary but not sufficient. A number can be faithfully quoted from the statute and still be wired into the wrong formula, or into the right formula with the wrong sign. So the encoding also has to compile, pass the companion tests that ship beside every rule, and clear a proof pass that checks the logic holds together—that the pieces refer to quantities that exist, in units that match, along paths that resolve. These are the unglamorous gates, the ones that catch the errors a careful person would eventually catch too, only faster and without getting tired. They establish that the encoding is internally coherent and externally sourced. They do not establish that it is correct.

For that, the encoding is raced against an oracle. An oracle, in this sense, is an independent implementation of the same law—usually built by other people, often over many years—whose answers we treat as a second opinion we did not write and cannot quietly influence. The oracles are the best independent tax-benefit models in the world. TAXSIM, the NBER calculator that has anchored academic tax research for four decades .^[2] The classic PolicyEngine engine. UKMOD, for the United Kingdom .^[3] EUROMOD, for the member states of the European Union .^[4] The SOUTHMOD family that UNU-WIDER maintains for a growing list of developing economies .^[5] And, wherever a tax authority publishes one, its own official calculator. Chapter 3 laid out three levels at which any such model is validated—component, aggregate, and predictive. What the oracle program does is take the first level, component validation, the one that used to mean spot-checking a married couple with $100,000 of income against an IRS worksheet, and industrialize it: replay entire populations through two engines and demand agreement on every record. It is component validation grown teeth.

There is a reason to race whole populations rather than a curated handful of cases, and it is not thoroughness for its own sake. A test suite a person writes tests the situations that person thought of. It will faithfully check the married couple, the pensioner, the family with three children—and it will say nothing at all about the case nobody imagined: the worker who crosses two thresholds in the same year, the household that lands in the seam between two rules, the combination that never came up in anyone's examples. Replaying a full calibrated population through two independent engines tests those cases too, because the population contains them whether or not anyone anticipated them. The pathological record that would otherwise have shipped undetected is precisely the one a broad enough replay puts in front of you.

What parity looks like

The United Kingdom is where the encodings and the oracle agree most exactly, and it is worth being specific about what "exactly" means, because the word gets used loosely. For a deterministic calculation there is a single right answer, and a tolerance band is mostly a comfortable place for a wrong answer to hide. UK income tax matches to the pound—not close, not within a tolerance, to the pound—across five test suites, including the awkward withdrawal of the personal allowance, the taper that claws back the tax-free band from high earners and produces the marginal-rate spike that trips up so much informal tax advice. The Scottish income tax, which runs on its own six-band structure, matches on nine cases out of nine. Savings income and dividend income, each taxed on its own schedule with its own allowances, match exactly. National Insurance matches or is explained: where the encoding and UKMOD diverge, the divergence traces to a documented convention—UKMOD computes contributions weekly and then annualizes, while the encoding works in annual terms—and once you account for the convention, the two reconcile.

Then there is Universal Credit, where the raw numbers look, at first, like a problem. Of nineteen Universal Credit test cases, eight matched. Eight out of nineteen would be a damning result if the eleven gaps were errors. They are not. UKMOD applies a stochastic take-up draw: household by household, it decides at random whether an eligible family actually claims the benefit it is entitled to, because in the real world many eligible families never claim. Our encoding computes statutory entitlement—what the household is owed if it claims. Those are different quantities by construction, and every one of the eleven mismatches resolves precisely to that difference. Nothing is wrong. The two systems are answering two different questions, and once you know which question each is answering, the gap is not a discrepancy but a definition.

This is where one word carries the load: disposition. In the conformance program, a raw mismatch is neither a failure nor a pass. It is an open question, and it stays open until it is closed with evidence. An explanation, in this vocabulary, is not a shrug and not a hand-wave. It is a checked artifact—an arithmetic reconciliation that reproduces the gap to the penny, a citation to the statutory provision the oracle implements differently, or a documented account of an oracle's own modeling convention, like the Universal Credit take-up draw. A mismatch is either dispositioned with one of those, or it is unexplained, and unexplained mismatches are the only kind that count against the encoding. Cast that way, the standing UK result is the one that actually matters, and it is not the raw match rate. It is this: across every compared surface, one hundred percent of mismatches explained, zero unexplained.

Belgium tells the same story through a different institution. The regional and municipal surcharges that sit on top of Belgian income tax match on nine cases out of nine. A greenfield encoding of student study allowances—a body of rules with no prior implementation anywhere to copy from—matches on six out of six. The contributions match per worker to three cents. Every mismatch on the Belgian conformance board carries its disposition, and none of them is attributed to an error on our side. The point of saying so is not to boast about a clean board. It is that "clean" here has an auditable meaning: not that nothing disagreed, but that everything that disagreed was run to ground and written down.

When the oracle is wrong

The dispositions discipline has a consequence we did not fully plan for. If every mismatch must be chased to evidence, then sometimes the evidence exonerates the encoding and implicates the reference model. Race a fresh, exhaustively grounded implementation of a law against a model that people have maintained by hand for years, and now and then the fresh implementation turns out to be right where the mature one is wrong.

What makes that possible is not cleverness; it is exhaustiveness. Nobody maintaining a mature model by hand replays tens of thousands of records against a second independent engine on every change—until recently the compute and the tooling to do it that cheaply did not exist. When you do, an inconsistency that surfaces in only a handful of unusual cases stops hiding in the tail of a distribution and shows up as a specific record with a specific wrong number, which is a thing a person can then investigate. The precision that catches float dust at three cents is the same precision that catches a genuine bug.

Chasing one such mismatch through the UK savings rules, we found the discrepancy was not in our encoding at all. UKMOD was mishandling an interaction involving the personal savings allowance—a corner of the rules where two provisions meet and the combined behavior is easy to get subtly wrong. We wrote it up the way the discipline demands: the inputs, the statutory result we expected and why, the reference model's actual output, and the provision each of us was implementing. Then we filed it publicly, as an issue on the UKMOD-PUBLIC repository, for its maintainers to weigh .^[6]

A second case was stranger. Running the EUROMOD comparison, we noticed that identical input cases were sometimes scoring differently depending on where they sat in a batch—the same household, the same year, two different answers, the result determined by its neighbors in the queue rather than by its own circumstances. That is the fingerprint of state leaking between records that are supposed to be independent, and we root-caused it to a batch-processing contamination bug in the adapter layer that runs cases through the model. We reported it to the maintainers with the reproduction in hand.

It would be easy to tell these as gotcha stories. They are the opposite. These reference models are the reason the encodings can be trusted at all; strip the independent second opinion away and "the machine says so" is exactly the epistemic position this whole project exists to escape. TAXSIM has been maintained for forty years. EUROMOD and its national variants represent decades of patient institutional work by the people who built the field of tax-benefit microsimulation in the first place. That a model of that size contains a bug is not a scandal—every large model does, ours emphatically included—and finding one is not a victory over its authors. It is what collaboration looks like when it runs in both directions. A reference model built and maintained across decades, in the act of validating a newcomer, gets something back that it rarely gets from anyone: free, specific, evidence-backed quality assurance from a system precise enough to notice a three-cent gap and disciplined enough to chase it to its cause. Openness means the errors flow both ways. We file our bugs upstream and theirs downstream, and both models come out better.

A one-way valve on correctness

The hardest honest objection to any public rules layer is not that it will be wrong on the day it launches. It is that it will rot. Laws change every year; the failure mode of shared infrastructure is not a dramatic collapse but quiet staleness—encodings that drift out of date as statutes move, coverage that erodes at the edges, a model that was accurate when it shipped and is subtly wrong three budgets later, with no one the wiser. Chapter 9 named that as the real governance fear, the one that durable funding alone does not answer. A verification suite that runs once and is admired is no defense against it. A verification suite wired into a ratchet is.

The conformance gates are configured as one-way valves. Coverage—the number of statutory surfaces under test against an oracle—may only rise; a change that would drop a jurisdiction or a program below its current tested coverage fails continuous integration and cannot merge. The count of unexplained mismatches may only fall; a change that introduces a new unexplained divergence, or that quietly un-explains one that was previously dispositioned, fails too. The count of ungrounded monetary obligations may only fall toward the zero it already reached. None of these numbers can slip the wrong way by accident, because the pipeline refuses to let a commit that moves them the wrong way in at all.

The valves hold because the full conformance suite runs on every change, not on a schedule someone has to remember to honor. When a new budget moves a threshold, the new value lands as a dated addition sitting beside the old one, and it has to pass against the oracle for its own year before the change can merge—last year's cases still checked against last year's law, this year's against this year's. Nothing is overwritten in place, so nothing quietly falls out of coverage when the parameters move. The moment the encodings drift from the law is the moment the build stops going green.

This converts an anxious, human, permanently-behind maintenance problem into a mechanical invariant. Staleness does not become impossible—a rule can still go un-encoded, a new program can still escape coverage entirely. But silent staleness does become impossible, and silence was always the dangerous part. The ratchet makes no promise that the encodings are complete. It promises something narrower and far more enforceable: that correctness, once won and checked, cannot be lost again without the build going red for everyone to see. That is a weaker guarantee than "always current," and a much stronger one than "trust us to keep it current."

The gates are for us first

It would be comfortable to describe all of this as a wall against untrustworthy AI—a filter that catches the machine's mistakes before they reach anyone. That is true, and it is not the honest emphasis. The gates catch our own mistakes first, and the most useful thing I can report about them is the times they turned red on us.

One premise we genuinely held, and set out to test, was that encodings are disposable. If an agent can encode a statute from source, the reasoning went, then any given encoding is just a cache: regenerate the module on demand from the underlying law and throw the stored copy away. It is an appealing idea, and it would have meant the artifacts barely mattered—only the source and the pipeline would. In July 2026 we ran the experiment. We took twenty-five existing modules, regenerated each one fresh from its source, and compared the new output against the version already in production. Regeneration was almost free, about eight cents of compute per module. The results refused to cooperate. Of the twenty-five, twenty-three came back with the old, in-production version correct and the freshly regenerated version worse—most often by introducing naming instability, renamed variables that would silently break every downstream consumer still referring to the old names. The premise failed. Encodings are not cache; they are durable artifacts with provenance, and regeneration, at least as we currently run it, is not yet trustworthy enough to be automatic. We know that not because we reasoned our way to it in advance but because a gate compared regenerated output to a known-good baseline and twenty-three of twenty-five came back wrong. The discipline told us something we would rather not have heard.

The deeper lesson was about provenance. An encoding is not just an answer; it is an answer with a history—which source it came from, which version of the law, which call was made where the text was genuinely ambiguous. Regenerating it from scratch discards that history and, worse, produces a new artifact that looks every bit as authoritative while quietly disagreeing with the one that every downstream system already relies on. Durability here is not sentiment about an old file. It is the property that lets a consumer trust that the number it read yesterday still means the same thing today, and that when the number does change, it changed because the law did.

It was not the only time. The benchmark from Chapter 8, the one that measures how badly language models do full household calculations, went through its own version of the same lesson. An early layer that narrated each result in prose was caught inventing derivations—in one case describing elderly enrollees as beneficiaries of a "non-elderly expansion"—and any audit that read those confident narratives inherited the fabrication whole .^[7] The fix was the same fix it always is: ground the explanation in the engine's actual internals, and add a validator that rejects any mechanism the underlying trace does not support. Even the audit layer needs ground truth; you give the judges traces, not prose. And when we adapted a US-calibrated population to the United Kingdom and wrote up the result, a summary statistic that no run had actually produced—a fabricated number—found its way into a draft and was caught at a verification gate before publication, and removed.

None of these is an embarrassing exception to an otherwise spotless record. They are the record. A verification regime that only ever vindicates the people who built it is not a verification regime; it is a marketing department with test coverage. The gates earn their standing precisely by the frequency with which they turn red on their own authors.

The admission rule

Underneath all of it sits a single rule, and it is the rule the rest of this book is built to honor. Simulation is admissible only where its verification chain terminates in ground truth—a forecast score, an oracle parity, a statutory exactness, a calibrated marginal. Not a plausible-looking number. Not a fluent narrative. Not an aggregate that lands in the right neighborhood. A chain of checks that bottoms out in something true independently of the model that produced it: a reference implementation, a quoted statute, a resolved outcome, an administrative total. Each terminus is a different kind of true thing, checked a different way. An oracle parity is the subject of this chapter—an independent implementation agreeing on every record. A statutory exactness is the money-atom carried to its end, an obligation traced to the quoted provision that fixes it. A calibrated marginal is an input distribution reconciled against a number the government actually counted, so the population the rules run on is not merely plausible but pinned to something real. And a forecast score is the terminus that only arrives later—a prediction with a published interval, graded when the official figure lands. They are not interchangeable, but they share the one property that makes any of them admissible: each bottoms out somewhere the model's own confidence gets no vote. Where that chain exists and holds, the estimate is admissible, and you can say how you know. Where it does not, the estimate—however fluent, however cheap, however fast the agent produced it—is confident fiction, and the honest move is to say so and mark the boundary rather than let the fluency stand in for the check.

Which surfaces the question this chapter has quietly leaned on the whole way through. Everything here rests on the existence of an oracle: a UKMOD to disagree with, a EUROMOD to file bugs against, an official calculator to match to the pound. The verification chain for an encoded rule terminates cleanly for the United Kingdom and Belgium and the United States because, for those places, a second opinion already exists. But most of the world's tax and benefit law has never been encoded by anyone, and for much of it no reference model exists at all—no calculator to race against, no mature implementation to disagree with, no independent answer to check. The discipline that makes the encodings trustworthy is built entirely on having something to check them against. What becomes of it where there is nothing?