Mechanical verification · Interactive explainer

How mechanical verification works

A drawn companion to the mechanical verification reference page. Eight scenes walk the standard: the three-part test evidence has to pass, the claim ladder and the denominator behind each tier, a metamorphic property you can check by hand, one kernel's full evidence stack, and the red controls that exist to prove the harnesses can fail. Every count on this page is a real count from the public repository. Written for auditors and engineers who have to defend a verification claim later.

Before stage 1 · Foundation

What counts as mechanical

BeginnerEvidence guide

Evidence counts as mechanical here when three properties hold at once. The claim names the check that produced it, so a verdict never floats free of its instrument. The check reads artifacts committed in the public repository, so what it read can be re-read later, byte for byte. And the check is deterministic, so anyone re-running it lands on the same verdict: pass, fail, or a specific finding.

Where a human judgment genuinely remains, chiefly whether a written specification reads the regulation faithfully, the estate validates the spec instead of signing it: the spec must reproduce the kernel's committed fixtures, and where a regulator publishes worked examples, as the FRB does for Regulation Z Appendix J, the spec must reproduce those too. What survives as judgment after that is stated on the claim itself.

the claim namesits checkverdict + instrument the check readscommitted artifactsre-readable, byte for byte the check isdeterministicsame commit, same verdict mechanical evidencere-runnable by anyone
three properties, all three required · drop one and the evidence is back to being somebody's assurance
Stage 1 of 7

The claim ladder

PractitionerEvidence guide

Every formal claim carries one of three tier statements, word for word, so the strength of a claim is never implied by vocabulary. The tiers are rungs: each one buys more coverage at a higher price to reach. Select a rung to see what it establishes and which kernels stand on it today.

L1 · enumerationall N inputs, nothing sampledart-157: 24 · art-27: 531,441 L2 · property testingidentities over stated rangesart-335: 10,000 trials per property L3 · machine-checked proofDafny port + differentialart-215, under published assumptions the fv-status recordwhich rung, machine-readable, digest-named
higher rungs cover more inputs at a higher cost to reach · the record beside the ladder says which rung each kernel stands on
Five kernels carry a formal claim today: two by enumeration, one by property testing, one by a machine-checked proof, and one by a hand proof the records describe plainly. No kernel outside the evidence guide's list carries a formal claim of any kind.
Word for word
The tier is part of the claim
A claim reads verified by exhaustive enumeration (all 24 inputs) or property-tested over stated ranges or machine-checked proof (Dafny). The count and the range travel inside the sentence, so nobody has to guess what was actually covered.
Complementarity
Tiers stack and never substitute
The APR kernel pairs its Dafny proof with a differential against the shipped kernel, because the proof covers the port and the differential covers the gap between port and kernel. One kind of evidence is an argument for the next, never a replacement.
Go deeper: The evidence guide, with each claim's wording → The fv-status records →
Stage 2 of 7

The denominator is the claim

PractitionerEvidence guide

The practical difference between tiers is the denominator: how many inputs the evidence actually touched. The agentic readiness diagnostic enumerates every one of its 531,441 states, twelve questions with three answers each, plus fourteen boundary states checked on top. The DTI ratio calculator samples 10,000 randomized trials per property over stated ranges. Each claim is stated to its own denominator, and the tier wording says which is which.

art-27 enumeration sweep · states checked
0
a browser tab re-derives the denominator in about two seconds; the sweep in CI runs every state on every push
enumeration3^12 grid: 12 questions, 3 answers each531,441 states, every one checked+ 14 boundary states on topwired into preflight: re-run on every push property testingdeterministic PRNG, stated ranges10,000 trials per propertyP1 monotonicity · P2 tier agreementP3 scale invariance · P4 ULP boundaries
the enumeration claim names its whole space · the property claim names its ranges · a third kernel, the EMIR validator, enumerates all 24 cells of a 3 × 8 legality table
Why enumerate
Small spaces make sampling a concession
When the whole input space fits in memory, running all of it is cheaper than arguing about a sample. The oracle recomputes each grade in a deliberately different way from the kernel's own loop, so a shared bug still surfaces as a divergence.
Why sample
Continuous spaces need ranges instead
A DTI ratio has infinitely many inputs, so the claim moves to the properties that must hold everywhere: monotonicity, boundedness, scale invariance, boundary behavior at the ULP level, each over a stated trial count anyone can re-run.
Stage 3 of 7

A property you can check by hand

BeginnerThe real P3

A metamorphic property compares outputs across a transformation of the input, with no oracle needed for the transformed case. The DTI kernel's P3 is the cleanest example: scaling income and every monthly debt by the same factor has to leave both DTI percentages unchanged, because numerator and denominator scale together. Try it: the panel runs a simplified one-line cousin of P3, the ratio itself, so you can feel the identity. The certified version runs 10,000 trials from a deterministic PRNG in the repository.

back-end DTI now
35.29%
after scaling both ×1.7
35.29%
identity holds
DTI % scale factor k 35.29 same ratio at k = .5, .7, 1, 1.3, 1.7 .5 .7 1.0 1.3 1.7
the identity's signature is a flat line · if the line tilts, some input no longer scales cleanly, and P3 goes red
No oracle needed
Why metamorphic checks are strong
Ordinary testing needs the right answer for every input. A metamorphic relation needs only the relation: the answer after the transformation must relate to the answer before it in a stated way. That works even where nobody can write down the right ratio by hand.
Stated scope
This panel is a cousin of the real P3
The demo above divides one number by another; the kernel's P3 drives the real compute() over 10,000 seeded trials and checks both DTI percentages. The gap between the two is deliberate and stated, the same way every claim here states its scope.
Stage 4 of 7

One kernel's evidence stack

PractitionerEvidence guide

The Regulation Z Appendix J APR kernel carries the estate's only machine-checked proof, and its stack shows how the layers lean on each other. Five committed vectors replay first. The property floor then runs convergence-or-report, termination, and a differential that re-derives the converged rate from the regulation's own residual. The Dafny port discharges proof obligations against a spec written from the regulation text, and the records pin the toolchain: Dafny 4.11.0 over Z3 4.12.1 and 4.14.1.

golden fixtures · 5 committed vectorsreplayed before any property runs property floor · P1 P2 P3convergence-or-report · termination · differential Dafny proof obligationsspec from the regulation text; port differentially tested fv-status recordtier, scope, assumptions, pinned toolchain, digest-named errata feedthe record checks itself against dated corrections
fixtures feed properties, properties feed the port, the port feeds the record, the record answers to the feed · each layer is a committed file anyone can open
the findingThe differential leg earned its keep once already: it surfaced an odd-days compounding divergence worth 0.456 percentage points of APR at 387.9%, the kernel was fixed, and the re-run differential now agrees to under 0.0001 percentage points across the range it exercises.
the gapThe proof covers the Dafny port, the rest of the stack covers the gap between port and shipped kernel. The record states the assumptions next to the claim: spec validation status, the port gap, and the pinned prover versions.
Go deeper: The floor file → The pilot record →
Stage 5 of 7

The harness has to be able to fail

AdvancedThe pilots

A harness that has never failed a thing has never shown it can. Two pilot families answer that with red controls: committed, deliberately broken copies of real kernels, run through the same harness to prove the alarm works. The boundary-metamorphic pilot checks that kernels sharing a threshold flip verdicts at the same point and in the same direction, 234 generated cases across four relations. Its control is a scratch copy of the QM points-and-fees kernel with exactly one comparator mutation, and running the pilot against it must go red, or the harness has detected nothing.

the real kernelsart-218 consumes the threshold art-220 publishesboth must flip verdicts at T, in the same direction relation holds · exit 0234 generated cases across 4 relationsdeclared expectations; surprises exit nonzero the red controla scratch copy of the QM kernel, its pass comparatormoved from at-or-under the limit plus a half cent to under it relation fires · alarm proventhe control run exits 0 only when themutated kernel trips the relation a fixture suite regenerated from the mutated kernel would agree with it; the relation between two kernels is what catches it
top lane: healthy kernels, quiet harness · bottom lane: the committed defect, the alarm sounds · the bottom lane is the harness proving it can fail
Why relations
Cross-kernel checks see a blind spot
A kernel's own fixtures are generated from its own tables, so they agree with a stale table just as readily as with a correct one. Where two kernels share a threshold, the relation between them is checkable and their fixtures alone never will be.
Pilot status
Deliberately outside CI and stated as such
Both families run on demand and report findings; a property failure is a finding to report, never a fix applied in place. Whether they become gates is a later decision, and the pilots say so on their own READMEs.
Run them: boundary-metamorphic pilot → cross-kernel consistency pilot →
Stage 6 of 7

Four commands from a fresh clone

Beginner

Everything on this page reduces to commands that exit zero on pass and nonzero on any failure. Plain Node, no package installation, deterministic results: your run lands on the same verdict CI landed on for the same commit.

fresh clonegithub.com/PostOakLabs golden fixtures · replay every committed vector property floor · every kernel, every property compute-proof coverage · vs its ratchet full preflight · every hard gate, CI order exit 0: passnonzero: finding
one clone, four gates, two exit codes · the interface is deliberately that small
git clone https://github.com/PostOakLabs/ainumbers
cd ainumbers

node chaingraph/kernels/golden-parity.test.mjs             # replay every golden fixture
node scripts/run-proptests.mjs                             # run the property floor, every kernel
node scripts/check-compute-proof-coverage.mjs --summary    # receipt coverage vs its ratchet
node scripts/preflight.mjs                                 # the full gate suite CI runs
Go deeper: How the property floor is run and scored →
Stage 7 of 7

Logic and execution are two different questions

Beginner

Mechanical verification answers the logic question: does this code compute what its validated specification says, over the inputs the claim covers. The Groth16 receipts answer the execution question: was this published output actually produced by running this code. A kernel can carry either kind of evidence, both, or neither, and the payee name-match kernel is the standing example of the split: it carries a hand proof of its termination and its recurrence, and no compute receipt, because string matching costs more than in-guest proving can currently handle, and its records state both facts.

the logic questiondoes the code compute what the validatedspecification says, over the claimed inputs?answered by: enumeration, properties, proofsthe mechanical verification page the execution questionwas this published output actually producedby running this code?answered by: a zkVM receipt, verified locallythe Groth16 receipts page claim, no receipt: art-376the payee name-match score receipt: proof-bearing kernelsevery one, in its node file either, both, or neitherthe coverage gate knows which
two questions, two evidence families · a kernel's records state which it carries, and which it does not
Clone and re-run the checks The prose reference The receipt, drawn

Sources: on metamorphic relations, Chen, Kuo, Liu, and Zhou, Metamorphic Testing: A Review of Challenges and Opportunities, ACM Computing Surveys, 2018. On small trusted checkers, Klein et al., seL4: formal verification of an OS kernel, SOSP 2009, project documentation at sel4.systems. Dafny: Leino, Dafny: an automatic program verifier for functional correctness, 2010, tool and documentation at dafny.org. Counts and findings on this page are from the repository's committed evidence files as of September 2026.