Mechanical verification: what it means and how to re-run it

Evidence counts as mechanical when three things hold. The claim names the check that produced it, so there is never a verdict floating 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 who re-runs it gets the same verdict: pass, fail, or a specific finding.

Where a human judgment genuinely exists, chiefly whether a written specification faithfully reads the regulation it claims to implement, we do not paper over it with a signature. The spec is instead validated mechanically: it must reproduce the kernel's committed fixtures, and where a regulator publishes its own worked examples (the APR rules in Regulation Z Appendix J, for instance), the spec must reproduce those too. What remains judgment after that is stated on the claim itself. An unauditable signature from the same party that drafted the spec would add nothing a third party could distinguish from signing every spec automatically, so the evidence has to stand on its own.

Stacking independent mechanical evidence sources is standard practice where correctness claims have to survive auditors: conformance suites built from the rule-maker's own computed answers (the approach NIST's cryptographic validation program takes), differential testing against an independently built implementation, metamorphic identities that must hold across whole input families, and machine-checked proofs discharged by a small trusted checker. The checks below use all of these.

Every formal claim about a kernel carries one of three tier statements, word for word, so the strength of the claim is never implied by vocabulary. These are the tiers; the kernels currently carrying each one are named on the formal-verification evidence guide, and no kernel outside that list carries a formal claim of any kind.

Every layer of evidence behind these claims is a file (or a whole directory of files) committed to the public repository. These are the paths, and what each one carries.

Five kernels carry a formal claim, and the evidence guide states each claim's wording. This section walks through the evidence files behind each one: what to open, what the file actually contains, and the command that re-runs it. Links go to GitHub, and the same paths work in a local clone.

The checks are plain Node with no package installation. Clone the repository and run any of them; each exits zero on pass and non-zero on any failure, which is the whole interface.

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   # compute-proof coverage vs its ratchet
node scripts/preflight.mjs                            # the full gate suite CI runs

The last one drives the complete pipeline and touches more surface than the three above it; the three targeted checks are the fastest way to see the evidence machinery move. Results are deterministic, so your run should match CI's verdict for the same commit.

Mechanical verification is about the logic: does the kernel compute what its validated specification says, for the inputs the claim covers. The Groth16 receipts are about the execution: was this published output actually produced by running this program. A kernel can carry either, both, or neither, and the coverage gate knows which. Neither kind of evidence substitutes for the other, and the payee-matching kernel above is the standing example: it carries a formal claim and no compute proof, and both facts are stated on its records. This evidence does not answer whether the regulation means what its worked examples show, a question neither a machine nor a signature has ever answered, and it stays inside the input spaces and ranges named in each claim. Whether a tool is right for your situation is a different question; see Terms & Reliance for the full disclaimer.

Sources: on oracle-aware evidence stacking, 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. NIST cryptographic validation program, csrc.nist.gov, accessed September 2026. All statements on this page are as of September 2026.