Methods

How outputs on AINumbers.co get checked

Being able to inspect how a result was produced is not the same as knowing the result is correct. This page explains how we check our outputs: six mechanisms, what each one covers, and where your own judgment still has to come in.

What gets checked

Six mechanisms, each narrow on purpose

No single mechanism here proves a tool is right for your situation. Each one closes off one specific way a result could be wrong, or could drift silently over time. Together they form the checking layer behind the OpenChainGraph-anchored tools. Simpler calculators without a ChainGraph node get the syntax and count-drift gates, but no compute proof.

Golden fixtures
A fixed set of inputs is pinned per kernel together with the output that kernel is expected to produce for them. A gate replays the fixture on every change and fails if the output moves.
Checks the kernel still produces the pinned answer for the pinned inputs. Not checked whether the pinned answer was correct in the first place, or whether inputs outside the fixture set behave the same way.
In-page rule citations
Where a tool implements a specific rule, standard, or regulatory formula, the page cites the governing text inline, dated, next to the calculation it applies to.
Checks which text the logic claims to follow, and when that citation was added. Not checked whether the implementation is a correct reading of that text. The citation names the source; it does not audit the reading of it.
Clause binding §28
Where shipped, a ChainGraph node's clause binding names the specific paragraph or line of the source text a computation implements, in machine-readable form (not just prose you'd have to parse).
Checks that a named clause maps to a named computation, and that mapping is queryable. Not checked coverage across the catalog. This page does not state what fraction of tools carry a clause binding, because that number changes with every release and a stated figure would go stale.
Conformance gate suite §15
Every push touching the OpenChainGraph data or spec runs a fixed suite: schema validation, spec-version consistency, gate coverage, spec-to-page parity, and golden parity. All five must pass before a change lands.
Checks internal consistency. The data matches its own schema, the spec, and its own prior outputs. Not checked whether the schema or spec themselves model the real-world rule correctly.
Deterministic replay
Given the same recorded inputs, the same kernel produces byte-identical output on re-run. There is no hidden state, no clock dependency in the calculation itself, and no server round-trip that could introduce variance.
Checks that the same inputs always give the same output, so a result can be independently reproduced later. Not checked whether the output is the right answer to the real-world question. Reproducibility and correctness are different properties.
Compute proofs §18
For eligible kernels, a zero-knowledge proof attests that the published output was produced by running the published kernel logic on the recorded inputs, without a third party needing to re-execute the kernel.
Checks that the specific computation ran as published, so a third party can trust the result came from that logic rather than being hand-typed. Not checked whether the kernel logic itself is a correct model of the rule. A proof over wrong logic still proves that wrong logic ran correctly.
Formal verification (pilot)

Four kernels are formally verified

Beyond the six mechanisms above, we run a formal verification pilot. Four of our kernels are formally verified: two by exhaustive enumeration of every possible input, one by a machine-checked proof in Dafny, and one by property testing backed by a hand proof. Each is verified against a specification that survived independent mechanical validation, and the assumptions sit next to every claim. As far as we know, no shipped product yet chains a complete functional spec, proved for all inputs, to a zk proof of faithful execution for general-purpose business logic. The two closest efforts are Pi Squared / FastSet, which proves interpreter semantics rather than arbitrary business-logic specs, and Horus (Nethermind), annotation-scoped verification for Cairo contracts, still alpha-stage. This pilot works toward that combined claim on the four kernels below.

We draft each spec with an LLM, from the regulation text itself and never from the kernel's code: a spec copied from the implementation can only prove the code matches itself. We then run the draft through independent mechanical validation: it must reproduce the kernel's golden fixtures, and where a regulator publishes its own worked examples, it must match those too. A spec that fails this validation goes back for another draft rather than forward to a proof. By the time a proof runs, the spec it proves against is the one that survived validation, so the check that matters is re-runnable by anyone, not a read of the text we are asking you to trust. One spec (the payee name-match scorer) was initially drafted the wrong way around, from the code instead of the declared contract. Validation caught the mismatch: we re-derived the spec independently from the contract, and the two versions matched, so the validated spec stands.

EMIR lifecycle event validator art-157
Verified by exhaustive enumeration (all 24 inputs). Every combination of action type and prior state was computed and checked against a mechanically validated spec, with zero failures.
Verified against a mechanically validated spec, under its stated preconditions, over the full declared 24-state space. Not checked anything about kernels outside this pilot.
Agentic-readiness diagnostic art-27
Verified by exhaustive enumeration (all 531,441 inputs). The full 312 answer-combination space, 12 questions with three answers each, was computed and checked against a mechanically validated spec, with zero failures.
Verified against a mechanically validated spec, under its stated preconditions, over the full declared answer space. Not checked: the roughly ten sibling diagnostics the same harness shape could in principle cover. They were not built or run in this pilot.
Reg Z Appendix J APR solver art-215
Machine-checked proof (Dafny). The solver's algorithm was ported to Dafny, and Z3 discharged the stated proof obligations, convergence of the bracketed solve, an explicit error bound, and preservation of iteration order over the fee/payment arrays, against a spec written from Reg Z Appendix J directly and mechanically validated against the regulation's own worked examples.
Checked that the ported model satisfies those obligations. Not checked by the proof itself: whether the shipped kernel computes the same function as the port. We test that separately by running the compiled proof and the shipped kernel side by side. That test originally found two discrepancies. We fixed both and re-ran it: the largest remaining divergence is under 0.0001 percentage points across the APR range exercised, well inside the tolerance Regulation Z §1026.22(a)(2) allows.
Payee name-match scorer art-376
Property-tested over stated ranges. A hand proof covers termination and the correctness of the underlying edit-distance recurrence, checked against the kernel's existing golden fixtures.
Verified against a mechanically validated spec for those two properties. Not checked: the surrounding normalization and scoring logic, which stays out of scope for this pilot. This kernel's fuzzy string-matching cost currently exceeds what the zk proving pipeline can practically handle in-guest, so it carries a formal claim without a compute proof. Those are two separate kinds of evidence, and neither substitutes for the other.
What the proofs assume

Spec correctness: each spec passed independent mechanical validation against the kernel's golden fixtures and, where the regulator publishes its own worked examples, against those too. The proof checks the code against that validated spec, not whether the regulation means what its worked examples show, a question no machine, and no signature, ever answered.

Port gap, art-215 only: Dafny proves properties of the ported model. Whether the port and the shipped kernel compute the same function is established separately, by differential testing, not by the proof. That test was re-run against the current kernel and found agreement well inside the §1026.22(a)(2) tolerance, as noted above.

Toolchain: the Dafny proof was discharged on Dafny 4.11.0 with Z3 4.12.1/4.14.1, pinned by digest in the underlying artifact. A different prover version is a different toolchain identity and would need to re-establish the result.

Runtime: the enumeration harnesses ran under Node v24.15.0 with no hidden state. A changed harness environment is, again, a different identity to re-check against.

This covers four kernels, named above, out of the catalog. No claim is made here about coverage of any other kernel or about compliance, and nothing on this page certifies, warrants, or guarantees anything about the tools that use these kernels.

Deploy provenance

The published bytes are signed to their build

The mechanisms above check computations; this one covers the road they travel to you. Each site deploy is published by a public GitHub Actions workflow from one named commit of the public repository. At publish time the deploy job hashes every file it ships into a manifest, served at .well-known/deploy-manifest.json together with the raw hash list it digests, and signs an attestation binding those bytes to that workflow run: an in-toto statement carrying an SLSA build-provenance predicate, signed under a short-lived Sigstore certificate and stored in the repository's attestation API. The attestation establishes that the tree served by this site came out of one named commit of that repository, built by the named workflow. It is a claim about process; the mechanisms above remain the claims about content. Two commands re-derive the process half from where you sit:

# fetch what the site is serving right now
curl -sO https://ainumbers.co/.well-known/deploy-manifest.json

# who signed these bytes, as JSON for policy engines; passes when the signing
# certificate's identity is the deploy workflow running on main
gh attestation verify deploy-manifest.json -R PostOakLabs/ainumbers --format json \
  | jq -e '.[] | select(.verificationResult.signature.certificate.subjectAlternativeName
           | contains("deploy-to-dreamhost.yml@refs/heads/main"))'

# recompute the digest: check out the commit named in the manifest, rebuild the
# hash list by the documented rules, then compare the served copy byte for byte
# and check its sha256 equals site_content_digest in the manifest. Rules: all
# repo files except .git, .github, scripts/, specs/, docs/, reconciled/,
# node_modules, editor and OS metadata, and *.md other than chaingraph/okf/**
# and chaingraph/standard/SPEC.md; sorted by path; sha256sum format.
sha256sum deploy-checksums.txt

# verifiers without the gh CLI can check the same attestation with slsa-verifier
Going deeper

Two pages, one per kind of proof

Two pages go deeper on the proofs themselves. Groth16 receipts walks through the zero-knowledge receipt embedded in each proof-bearing node, field by field, reads one real receipt from the repository step by step, and shows four ways to verify one. Mechanical verification explains the standard behind our formal claims, walks through the evidence files for each of the five kernels that carry a claim, and lists the commands that re-run every check. SPEC.md remains the normative definition of every mechanism named on this page.

Browse the ChainGraph hub Groth16 receipts Mechanical verification Read SPEC.md ↗