learn / no prerequisites
the streetlight
and the proof.
Every protocol that ever rugged you was "audited." Sit with that. The bridges, the vaults, the lending markets drained for nine figures — audited, stamped, reviewed by prestigious firms. And still zeroed. This page explains, with no math required, what an audit actually is, what a proof actually is, and why they are not the same sport.
what an audit actually is
Smart people read your code and try to break it. They're good at it. But here's the part nobody says out loud: they check examples. They poke the cases they can think of, run some tools, trust their gut. And when they don't find a bug, they write "no critical issues found."
Read that again. No issues found. Not no issues exist. They looked under the streetlight. The bug that drains you is the one standing in the dark they didn't think to check. Your contract has infinitely many possible inputs; an audit checks a handful. That gap — between "we looked hard" and "it's actually safe" — is where every exploit in history has lived.
formal verification, in one breath
Instead of checking examples, you write the rule down in math — "this vault can never pay out more than was put in" — and then you prove it, like a theorem, for every possible input, every possible state, forever. And a machine checks that the proof is airtight. No gut, no vibes, no "should be fine." If the proof goes through, there is no input that breaks the rule. Not "none found." None exist.
testing
Checks that 2+2=4, and 5+3=8, and 10+10=20, and goes "yeah, addition works." A sample. Testing can only ever show a bug is present.
proof
Proves a+b = b+a for all numbers at once. Covers infinity. Proof is the only thing that can show a bug is absent.
So: "audited" means someone looked and didn't see it. "Formally verified" means it is mathematically impossible.
the honest part, said out loud
Formal verification is not magic. It proves your code does what the spec says — and the real ones say the two catches out loud.
catch one — the spec
You have to write the spec right. Prove "the vault conserves money" but forget "and only the owner can withdraw"? Congratulations — you proved the wrong thing, airtight. Garbage spec in, garbage guarantee out. (This is why dregg's specs carry non-vacuity witnesses — each property is proven able to fail, then proven not to.)
catch two — the floor
It stands on a small floor: the crypto (hashes, signatures) and the hardware. You don't prove those; you assume them. But it's a tiny, named, public floor — not "trust the 40k lines and the dev." It's "trust these primitives and this written-down spec — and here, go check them yourself."
That's the actual flex. Not "trust me bro, it's safe." It's: here is exactly what I proved, here is the little floor I'm standing on, and you don't have to believe me — the proof is right there. Run the checker.
the four words, in plain words
cell
A little world that belongs to someone. It holds money, data, powers, and its own history. Your account is a cell; a document is a cell; an app is a cell; an AI agent's mind can be a cell.
turn
One move. Everything that ever happens is a turn: send, save, vote, spend. A turn either fully happens or fully doesn't — and it only happens if the mover can prove they're allowed.
capability
A power you can hold, shrink, and hand on — but never inflate. Give a friend "read my photos for a week" and that grant can't quietly become "read everything forever." Mathematically can't.
receipt
The trail every turn leaves. Anyone can check a receipt without trusting the machine that produced it — and a light client can check all of history by checking one small proof.