Formal Verification: Proving Code Correct

An audit says “we looked hard and found nothing.” Formal verification says “we proved this can never happen” — but only for the exact things you thought to state.

Crypto & Tokenization · Lesson 41 · 11 min read

Lesson 39 left us with a hard truth: an audit can find bugs but can never prove there are none. That’s frustrating for code holding billions with no undo button. So a natural question: is there any way to get an actual guarantee, not just “experts looked and didn’t find anything”? There is — a powerful and often misunderstood technique called formal verification — but it comes with a catch so important that misunderstanding it is dangerous. Hold the question: how could you prove a program can never misbehave — and what would such a proof still fail to protect you from?

Testing samples; verification proves

The difference from ordinary testing (and even auditing) is fundamental. Testing tries a sample of inputs and checks the results — useful, but it can only ever cover the cases you actually run, so a bug in an untried case slips through (the “can’t prove absence” problem from lesson 39). Formal verification instead uses mathematics to prove that a stated property holds for every possible input and state at once — not by trying them, but by reasoning about the code the way you’d prove a theorem. If the proof succeeds, that property is guaranteed, forever, for all inputs — a genuinely stronger assurance than “we tested a lot and it seemed fine.” It’s the difference between “I checked a hundred cases” and “I proved it for all of them.”

The heart of it: invariants

What do you prove? Usually invariants — properties that must always be true, no matter what. For a token contract, a classic invariant is “the sum of everyone’s balances always equals the total supply” — if that could ever break, tokens are being created or destroyed from nowhere (a catastrophic bug). Or “no one can withdraw more than they deposited.” Formal verification proves such statements hold across every sequence of operations an attacker could try. This is powerful precisely because the exploits from earlier lessons — reentrancy draining more than you own (lesson 37), an oracle trick unbalancing the books (lesson 38) — are exactly violations of invariants. Pin the right invariants and prove them, and whole categories of bug become provably impossible.

Verifying a token’s core invariant:
• Invariant to prove: “sum of all balances == total supply, always.”
• A reentrancy bug that pays an attacker twice would break this — balances would exceed supply.
• If formal verification proves the invariant holds for every possible call sequence, that class of drain is proven impossible — not “not found,” but impossible.
• That’s a guarantee an audit alone can never give.

The catch: you only prove what you specify

Here’s the danger, and it’s the whole reason this needs its own lesson. Formal verification proves your code satisfies the properties you thought to write down — and nothing else. If you forget to specify an important property, the proof says nothing about it, and a bug can live happily in the unspecified space while the contract proudly claims “formally verified.” The hard part isn’t running the proof; it’s writing the correct, complete specification of what “correct” even means — and that’s a human judgment as fallible as any (a subtle cousin of the prompt-specification and garbage-in problems elsewhere). So the honest framing: formal verification gives an ironclad guarantee about the exact things you specified, which is enormously valuable for the core, high-value logic (where it’s worth the considerable effort) — but “formally verified” is not “provably safe overall,” because it can’t cover what you didn’t think to state. It’s the strongest tool in the box and still not a magic wand — which is why serious projects layer it with audits, bounties, and limited exposure (lesson 39). Proof beats searching, but only for what you knew to ask.

Where formal verification helps — and where it doesn’t:
1. Core logic (token balances, a vault’s accounting): specify tight invariants and prove them → whole classes of drain become provably impossible. Worth the effort.
2. A forgotten property (say, an edge case in how fees round): never specified, so the proof is silent — a bug can live there despite “formally verified.”
3. Takeaway: the proof is only as good as the spec, so it’s a powerful layer, not a full guarantee.
4. That’s why even formally-verified protocols still run audits and bug bounties (lesson 39).