Forty-four certificates, and the war we declared on our own green light
A month ago, each of our four formally verified ed25519 signature libraries carried sixteen machine-checked theorems. Today each carries forty-four — the entire tower from raw byte arithmetic up through the elliptic-curve group law, the scalar arithmetic, and the four capstone theorems that say "the verifier accepts exactly when the math says it should." That tripling is the headline. It is not the story.
The story is a button.
Every one of our repositories has one: a script you run, which recompiles every proof from nothing, asks the proof-checker's kernel what every theorem really rests on, and prints ALL GREEN if everything holds. The proofs are mathematics; the kernel is famously paranoid; nothing gets past it.
But the button is not mathematics. The button is ordinary software, written by us — and a green light is only worth what the thing switching it on is worth. So we invited outside reviewers — strong ones, both human-style and machine-style — to attack not our theorems but our button. Round after round. Nine rounds so far.
They never broke a theorem. Not one, in any round. What they broke, repeatedly, was everything around the theorems. A stubbed-out helper that made the button print ALL GREEN over deliberately destroyed proofs — in 3.6 seconds. A checker that quietly skipped work when a file was missing, and counted the silence as success. A tally that said "0 problems" when the truthful sentence was "0 things were examined." Our own status reports to the reviewers got numbers wrong — so we built a findings register where every defect is recorded in the reviewer's own words, and the tool that renders it refuses to run if the register is internally inconsistent. That tool has since rejected us, twice. Good.
Out of all this came a discipline we now apply everywhere, and which you can read in the repositories' own trust documents:
- Never trust a light you can't re-derive. Every count the button prints
is checked against the real population it claims to count — in both directions, so nothing can hide by being absent.
- Silence is failure. If a check couldn't run, that is a red light, not
a shrug.
- The gate must be shown to reject. For every check, there is a test
that deliberately breaks the thing and demands the button catch it. A gate that has only ever said yes proves nothing.
- Write down what is NOT covered. Each repository carries a trusted-base
document that lists, bluntly, what the proofs do not establish — including the fact that we prove signature checking and never signature making.
The forty-four certificates are why you might trust the libraries. The month of self-inflicted attacks is why you might trust the claim. And if you'd rather not trust either: every repository has the button, and the button runs on your machine too.