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. The lasting public copy of a receipt (the RECORD) lives on a11oy.net. This site’s /verify page is the interactive checker on a-11-oy.com. Those are two different hosts with two different jobs; they are not merged, and the unhyphenated furniture shop is not ours.
Four tiers. Kernel locked-proven from /api/a11oy/v1/honest; catalog counts 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". The locked-proven chip is the Lean-8 kernel, not the genome catalog tag LOCKED-PROVEN (a larger catalog count). The labels are conservative on purpose, so a buyer's auditor finds the math is stronger than the label, never weaker.
Locked-proven · kernel
Bound from /api/a11oy/v1/honest locked_formula_count
(ids F1,F4,F7,F11,F12,F18,F19,F22). Not the genome catalog tag LOCKED-PROVEN.
SEMANTIC-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 — advisoryGenome catalog (not the kernel): LOCKED-PROVEN tag = — of — entries. Never shown as Lean-8. Never green.
Loading 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.
Rows are the /honest locked-formula ids; genome supplies the catalog text for those ids only.
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.