The second act: how a green light can lie without a single wrong theorem
Here is a number pair that changed how we think about formal verification. Proving eleven theorems about a post-quantum signature verifier took two days — and across every adversarial review since, not one theorem was ever disputed. Making the sentence "this is formally verified" checkable by a hostile stranger took months, and produced dozens of registered defects.
Zero defects in the mathematics. All of them in the evidence.
We've come to describe verification as two acts. Act one: a proof checker (ours is Lean) accepts your theorems. That part is mathematics, and it is nearly incorruptible. Act two: binding what the checker accepted to the claim you publish — the exact statements, the exact version of the code, the exact assumptions — so that a stranger who does not trust you can re-derive all of it. That part is engineering, and it fails in ways the proof checker cannot see, because the proof checker was never shown your claims.
The most instructive failure we inflicted on ourselves: a reviewer replaced one small helper script in the repository, and our one-command verification — the button that rebuilds and audits everything — printed its full green verdict over deliberately destroyed proofs in under four seconds. Every theorem was garbage; the light was green. The button checked the proofs; nothing checked the button.
Every act-two failure we found has the same shape: something load-bearing sat outside the binding. The list of theorems to audit — outside. The script doing the auditing — outside. The assumptions policy — outside. Each round of review found the next thing sitting outside, and each fix drew the boundary around it, until the audits began auditing themselves.
If you take one idea from this post: when someone says "formally verified," ask the second-act questions. Which exact statements? About which exact code? Resting on which assumptions? And can I re-derive that myself, without trusting you? A proof without those answers is a private conviction, not public evidence.
We are developing this into a second paper — a field guide to the ways a green light lies, and the engineering laws that stop it. The living system these ideas run on is public today: ltl.zkdefi.org, where every claim carries its exact statements and assumptions, and one command re-checks the entire ledger that holds them.