How the formal-verification pilot actually works

A candidate spec is drafted from the cited regulation text itself, never from reading the kernel: a spec derived from the implementation would only show that the implementation matches itself. Every spec file in this pilot carries the clause's source document, the date it was retrieved, a content digest of that document, and a stored snapshot location, so the exact text a spec claims to implement can be checked later even if the live regulation page changes. One kernel in this pilot, the payee name-match scorer, deviated from that order in its first draft; the deviation was self-disclosed, the spec was independently re-derived from the declared contract 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. Where a stronger public oracle exists, the pilot uses it, for example Appendix J's own four worked transactions, matched to two decimals before any proof is trusted. The negative control is the gate that actually earns trust: a spec that never fails, even a spec deliberately built wrong, is not verifying anything. Mutation and vacuity checks close that gap by confirming the spec's obligations are strong enough to catch a broken proof, not merely present.

The proof itself is never what a human adjudicates; by the time a proof runs, the spec it proves against is already the human-signed artifact. Today's process runs under a stated single-adjudicator assumption: the person who prompted a spec's drafting and the person who signs it are the same person, and no other person reviewed it. A routine template instance of an already-signed spec family may publish provisionally under a named review-cadence challenge window rather than wait for a fresh pre-sign; a novel spec is always pre-signed before its proof is trusted. Nothing about the window implies a stake, a bond, or an adversarial dispute; it is a labeling and review-cadence device, and today the only reviewer able to challenge within it is the same signer.

These are Tim's own tier labels, used verbatim, not a marketing paraphrase of them. "Verified" always ships with the spec and its stated assumptions visible next to the claim, never as a bare word standing alone.

A proof is only meaningful bound to the exact code, spec, and toolchain that produced it: the kernel's content digest, the signed spec's digest, and the pinned toolchain digest (Dafny and Z3 versions, for the Class C leg) are each checked at proof time. Execution itself runs through the same zk compute-proof and runtime-twin machinery the rest of the suite uses; this page doesn't duplicate that mechanism, 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, discharged against a spec drafted from Appendix J's text rather than the kernel, went further: it found that 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 and growing to a measured 5.56 percentage points at the most extreme rate probed, breaching the §1026.22(a) tolerance above roughly 200% APR with a near-full odd-day fraction. 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 were computed. Both are documented findings against the specification, tracked for kernel repair as a separate landing step, not silently patched into this page. See Methods for the pilot's present canonical status per kernel.

See the Terms & Reliance page for the full disclaimer, and Methods for the six general-purpose checking mechanisms this pilot sits alongside.