Trust you can check, not trust you're asked to take.
a11oy signs its work and refuses to lie. This page is the inverse of a green badge: every claim below is tied to a machine-checkable artifact — a named Lean theorem, a live endpoint, or a receipt you can verify yourself, offline, with a hash function and our public key. Where we have not proven something, we say so plainly. A conjecture is never rendered as proven.
Four tiers. Counts are read live from /api/a11oy/v1/genome.
Every formula in the genome carries exactly one tier. The tier says precisely how strong the claim is — from a kernel-checked Lean theorem down to an honest "no proof claimed". This is the moat: the labels are conservative on purpose, so a buyer's auditor finds the math is stronger than the label, never weaker.
LOCKED-PROVEN
In the frozen locked-8 baseline (Wave11). Each labelled with what the Lean obligation actually proves — conservative Nat/Int surrogates, not the governance prose they motivate.
kernel-checkedSEMANTIC-VERIFIED
Sorry-free real theorems proving a governance property, outside the frozen baseline: the Λ aggregate bounds, Theorem U (conditional), DSSE verifiability. This is where the real trust math lives.
machine-checkedEVIDENCE-BACKED
Real runtime/algorithmic code with tests and live endpoints, but no formal proof claim. Honest operational tier — never dressed up as proven.
runtime / testedCONJECTURE / ADVISORY
Λ unconditional uniqueness = Conjecture 1 (machine-checked false as stated). BFT safety = Conjecture 2, liveness = Conjecture 3. Rendered gray. Never green.
open — advisoryLoading live counts from the genome endpoint…
What the frozen baseline actually proves.
The console once labelled these as semantic governance theorems with anchor files that
do not exist. The truth is more modest and more defensible: the locked-8 live in
Lutar/Puriq/Formulas/ProvedFormulas.lean and prove conservative arithmetic
surrogates. We label each with what it proves — and, in red, the overclaim it is not.
Rendered live from the genome's LOCKED-PROVEN tier.
SEMANTIC-VERIFIED: sorry-free theorems, outside the frozen baseline.
These are the proofs that actually govern trust. They are not in the locked-8 set, but they are real, kernel-checked, and zero-sorry. We present them proudly and precisely — including the one axiom we depend on, disclosed.
The Λ uniqueness question, answered honestly.
Λ is our 13-axis weighted geometric-mean trust aggregate (advisory, floor 0.90). People ask: "is Λ the unique correct aggregate?" The honest answer has two halves — one proven, one open.
Theorem U — conditional uniqueness
Under a stated separability hypothesis, Λ is the unique aggregate satisfying the axioms.
This is a real, sorry-free Lean theorem. The bounds min ≤ Λ ≤ max are also
proven (Λ_le_max, min_le_Λ, 0 sorries).
Lutar/Bound.lean::Λ_le_max · ::min_le_Λ
Unconditional uniqueness — NOT proven
Drop the separability hypothesis and the claim is machine-checked false as stated
(maxAgg_ne_Lambda is a counterexample witness). So unconditional Λ-uniqueness
is Conjecture 1 — advisory, never a theorem, never rendered green. We surface it as open
precisely because hiding it would be the lie.
SLSA: L1 honest, L2 attested, L3 roadmap.
We state the supply-chain level we actually hold, and link to the live disclosure so you can check it. We do not claim L3, Iron Bank, FedRAMP, CMMC, or ATO — those are roadmap.
The deployed image is cosign-signed and publicly verifiable (Rekor inclusion). Real signature, real transparency-log entry.
Signed SLSA build-provenance attestation (Sigstore keyless, Fulcio+Rekor), verifiable
via gh attestation verify / cosign verify-attestation. Emitted,
not third-party audited.
Hardened, isolated, fully-attested build with non-falsifiable provenance. Not yet held — labelled ROADMAP, never green.
Don't trust this page. Check it.
The button below makes a real POST /api/a11oy/v1/govern/infer call, then verifies
the returned DSSE ECDSA-P256 signature in your browser with WebCrypto — no
server round-trip for the verification. It recomputes SHA-256 of the decoded payload and the
DSSE PAE, and checks the signature against the matching public key. A flipped byte fails.
Offline path: save the receipt JSON, then verify with the public key and any DSSE/cosign
tooling — cosign verify-blob --key cosign.pub --signature <sig> <payload>.
The full multi-section flow (honest refusal, thesis) lives at /verify.