How the formal-verification pilot actually works

We draft each candidate spec from the cited regulation text itself, never from the kernel's code: a spec derived from the implementation can only show the implementation matches itself. Every spec file records the clause's source document, the date we retrieved it, a content digest, and a stored snapshot location, so you can check the exact text a spec implements even after the live regulation page changes. One spec (the payee name-match scorer) was initially drafted the wrong way around, from the code instead of the declared contract. We caught it, re-derived the spec independently without reading the kernel, and the two versions matched, so the signed spec stands.

The kernel's own golden fixtures are the obvious oracle, and a weak one: a spec transliterated from the kernel passes them trivially. So where a stronger public oracle exists, we use it. Appendix J publishes four fully worked transactions, and a spec has to reproduce them to two decimals before we trust any proof against it. The negative control is what actually earns trust: a spec that can never fail (even one we deliberately built wrong) isn't verifying anything. Mutation and vacuity checks close that gap by confirming the spec's obligations are strong enough to catch a broken proof.

By the time a proof runs, the spec it proves against has already cleared every gate above: the fixture-oracle check, the negative control, and the spec-strength checks. Each gate is a script anyone can re-run against the same spec and the same fixtures, and each result is recorded in that kernel's evidence vector alongside the gate that produced it. A person still drafts and reads every spec, today the same person who prompts its drafting, and we state that wherever it is relevant. What changed is what a verified claim rests on: the gate ladder, not that reading.

These tier labels are our own, and we use them verbatim wherever a kernel's status appears. "Verified" always ships with the evidence vector and its stated assumptions visible next to the claim.

A proof only means something when it is bound to the exact code, spec, and toolchain that produced it. So at proof time we check three digests: the kernel's content digest, the signed spec's digest, and the pinned toolchain digest (the Dafny and Z3 versions, for the Class C leg). Execution itself runs through the same zk compute-proof and runtime-twin machinery as the rest of the suite. See How the Kernel VM Works for how one kernel source runs identically across runtimes and what execution_hash agreement actually checks.

Reg Z Appendix J publishes four fully worked transactions with their APRs. The shipped kernel reproduces all four to the two decimals the regulation itself speaks in, and its own three golden fixtures pass unchanged. That is the entire evidence a fixture-only check would ever produce. The Dafny proof went further, because its spec was drafted from Appendix J's text rather than from the kernel. It found the kernel compounds interest across an odd-days fraction where Appendix J (b)(6) and (b)(8) prescribe simple interest: a deviation invisible at ordinary rates that grows to a measured 5.56 percentage points at the most extreme rate probed, breaching the §1026.22(a) tolerance above roughly 200% APR. Separately, the proof's solver harness exposed a Newton-iteration exit that could mark an unconverged result converged: true, returning the caller's own guess as if it had been computed. Both are documented findings, tracked for kernel repair as a separate step. See Methods for each kernel's current status.

The scope stays deliberately narrow. Existence of the root is not claimed: for the APR solver, Dafny's real type is rational and the root is irrational, so uniqueness and the bisection bracket are proved, existence itself is not. Date arithmetic is out of scope; deriving day counts and period fractions from calendar dates is neither in the spec nor proved, and it sits outside this pilot entirely. The Class C floor is not the same claim as a proof: the site-wide property-test floor (below) is internal engineering QC over a much larger kernel set, a different, weaker guarantee than this pilot's four mechanically validated, proved kernels, and it is never presented as equivalent to them. Mechanical validation is bounded by what the regulator publishes: each spec is checked against the kernel's own fixtures and, where one exists, the regulator's own published worked example, and whether the regulation means what its worked examples show is a question neither a machine, nor a signature, ever answered. Conformity of the shipped kernel to the clause is a separate question from spec correctness: a proof over a Dafny port establishes the port satisfies its obligations, while whether the shipped JavaScript computes the same function is checked separately, by differential testing, exactly as Panel 6 shows it can diverge. Coverage is four kernels, named, out of the catalog; no claim is made here about any other kernel, and nothing on this page certifies, warrants, or guarantees compliance with any regulation.

See the Terms & Reliance page for the full disclaimer, and Methods for the six general-purpose checking mechanisms this pilot sits alongside. The technical white paper covers the full verification ladder this pilot is one rung of.

Some gates in this codebase shield known, already-reviewed debt behind a committed baseline file rather than blocking the build outright. A baseline records exactly what already existed when the gate went live; a new violation fails the build immediately; the baseline itself may only shrink over time. This table is produced by scanning the repository for every file that follows that pattern, so a newly added baseline is picked up automatically the next time this page regenerates, and a retired one drops off the same way. Each count below is read from the named file at generation time; none of it is entered by hand.

Last changed is the most recent commit date on that file, so a class that has been still for a long time reads as stable and one that moved recently reads as active. The trend for any class is the git history of its own file, linked above; this page keeps no separate time series.

A separate, estate-wide checker asks a narrower question about every chain: does each step's decision gate read a value the producing tool's published output actually guarantees, and the consuming step's published input actually assume? This is "L2: contract composition" on our own verification ladder: assume-guarantee composition against published manifest schemas, never an execution of any kernel.

Contracts are checked against the published schemas and the cited primary text; whether the regulation means what its text and worked examples show is a question no machine and no signature has ever answered. No kernel becomes more correct because its chain composes, and a perfectly composed chain can still be the wrong workflow for the rule. This is not formal verification: L2 checks declared assume-guarantee composition only, no kernel is ever executed, and end-to-end chain properties (L3) remain a separate, unbuilt tier. Nor does it check that one step's output flows into the next step's input at runtime; chains are provenance-linked bundles of independently parameterised kernels rather than data pipelines, and each step's inputs come from the caller or a fixture, never the prior step's output.