Five kernels out of the suite's 578 carry formal-verification evidence today, produced by three different methods: exhaustive enumeration, property-based testing, and one machine-checked Dafny proof. This guide states plainly what each method establishes, what it does not, and how it relates to the suite's separate zk execution receipts. No kernel outside the five named here carries a formal claim of any kind.
The claim above is narrow on purpose. Two projects come close to it from different directions, and both are worth naming rather than waving away.
Proves interpreter semantics rather than arbitrary business-logic specs. Its claim-envelope model, evidence attached to a claim rather than a new envelope type, is the pattern this suite's own artifact schema borrows. Canonical Proof-of-Proof documentation was removed after a rebrand; anything sourced only from that removed documentation is marked unverified wherever it is cited.
Annotation-scoped formal verification for the Cairo language, alpha-stage, AGPL-licensed. Its clause vocabulary, preconditions and postconditions with a bound result variable, invariants, boundary cases, is cited below for design attribution only. No Horus code is vendored in this repository; AGPL forbids it, and none was read.
578 kernels were classified by input shape (48 exhaustively enumerable, 243 bounded-numeric, 287 unbounded). Five were carried through a verification pilot. The methods are not equivalent to one another, and the table states each one's actual strength rather than a single blended label.
| Kernel | Method | Public claim |
|---|---|---|
art-157EMIR lifecycle event validator |
Exhaustive enumeration, 24 states (8 action types × 3 prior states), 0 failures | Class A Verified by exhaustive enumeration (all 24 inputs) |
art-27Agentic readiness diagnostic |
Exhaustive enumeration, 312 = 531,441 states, 0 failures, 14 boundary states checked separately | Class A Verified by exhaustive enumeration (all 531,441 inputs) |
art-335DTI ratio calculator |
Property-based testing, 5 properties × 20,000 trials each, 0 violations, plus 15 forced floating-point boundary cases | Class B Property-tested over stated ranges |
art-215Reg Z Appendix J APR |
Dafny 4.11.0 + Z3 machine-checked proof of three obligations, compiled to JS, differential-tested against the shipped kernel | Class C / Dafny Machine-checked proof (Dafny), with a known divergence disclosed below |
art-376Payee name-match score |
Hand-proof of loop termination and DP-recurrence correctness (Wagner-Fischer); never run through a proof assistant | Hand-proof Verified against the stated termination and recurrence-correctness properties; never machine-checked |
Every other kernel in the suite carries no formal-verification claim of any kind. Its execution can still carry a zk receipt attesting that a specific input produced a specific output under a specific code hash; that is a different evidence type, described in the composition section below.
The Dafny spec for art-215 was written from Reg Z Appendix J directly rather than transliterated from the shipped kernel, and its oracle gate reproduced the regulation's own four worked examples exactly before anything else was trusted. Running the proof against the shipped kernel's behaviour surfaced a real, unfixed divergence: the kernel compounds an odd-days interest fraction where Appendix J (b)(6) and (b)(8) prescribe simple interest, which overstates the calculated APR above roughly 200% APR (0.456 percentage points at 387.9% APR), while still matching all four regulation worked examples at two decimal places.
Each verification word on this page maps to a specific evidentiary strength, following the ISO/IEC/IEEE 24765 (SEVOCAB) split between "verification" ("specified requirements are fulfilled") and "validation" ("fit for intended use"), and the DO-333 framing that formal analysis discharges named, stated verification objectives rather than blessing a kernel wholesale.
proven: reserved for a named, machine-checked theorem. Only art-215's three Dafny obligations qualify. It is never used for enumeration, property testing, or a hand-proof.verified: always carries an object, verified against spec S, under assumptions A. Never used bare.validated: spec-level review or testing that the spec itself is fit for its intended use. This word collides with a second, unrelated sense in banking: SR 11-7-lineage "model validation," a distinct regulatory review process. Where both senses could apply to the same reader, this guide names which one it means.correct / bug-free: never used bare, for any kernel, regardless of evidence tier.exhaustively checked: the honest phrasing for a class A enumeration. A stronger claim than property testing, but not a theorem, and the checked state space is always named.LLM-drafted, verifier-checked: the exact phrase used wherever a language model assisted drafting a spec or harness. The checker is the trust anchor rather than the model. "AI-verified" is never used.Following the disclosure shape used by seL4's own "what the proofs assume" page, every verification artifact in this pilot rests on the same four unproven layers. Naming them is part of the claim rather than a footnote to it.
Every spec file was authored from a cited clause and independent fixtures, never by reading the kernel and restating its behaviour. A spec that mirrors the implementation would prove only that the implementation matches itself. The clause reading itself is a human act and is not proved.
For art-215, the Dafny model is a port of the shipped kernel's logic rather than the shipped bytes themselves. The proof covers the port; a differential test against the shipped kernel on real fixtures is the evidence connecting the two, and it is where the divergence above was found.
Dafny 4.11.0 compiled against Z3 4.12.1 and 4.14.1. Every verification artifact pins the exact toolchain versions used; a version change invalidates the binding and requires re-verification, the same discipline already applied to kernel-digest changes.
The compiled JavaScript runs in the browser's own numeric runtime (IEEE 754 double-precision floating point), which Dafny's real-number arithmetic approximates rather than models bit-for-bit. Boundary and floating-point-sensitive cases are tested separately for exactly this reason.
Every kernel in this suite is a pure function: reads its declared inputs only, modifies nothing, holds no state between calls. That is stated explicitly for each verified kernel rather than left implicit, because an omitted frame condition is a classic audit gap in formal-methods writeups: a reader who never sees the claim "modifies: nothing" has no way to know whether it was checked or simply never considered.
Dafny and Z3 are not trusted by assertion. The method-soundness argument follows the DO-333 (RTCA) framing for qualifying a formal-methods tool: the prover's soundness is a property of the method, cited by reference rather than re-derived here, and every artifact pins the exact tool versions used (above) so a future soundness issue in a specific release is traceable to the artifacts it affects.
This suite separately produces zk execution-hash receipts, attesting that a specific input produced a specific output under a specific, hashed code path. Formal verification and that zk leg are two separate evidence types over the same underlying claim, "this shipped kernel computes what it says," and neither replaces the other.
| A zk execution receipt shows | Formal-verification evidence shows |
|---|---|
| This one declared input produced this one declared output, under this exact code hash, without re-running the computation to check it. | The kernel behaves correctly across an entire stated domain (a full enumerated space, a property tested over stated ranges, or a machine-checked theorem) rather than only for the input that happened to be run. |
| Available today for any kernel in the suite that supports it, including ones with no formal-verification evidence at all. | Available today for five kernels only. The art-376 payee-match kernel is a documented case of a kernel that current zk tooling cannot reach at all, yet it still carries a hand-proof correctness claim, exactly the complementary shape this section describes. |