What is Formal Verification?
Formal verification is the mathematical proof that a smart contract's code correctly implements its specification — providing the highest level of assurance that code behaves as intended under all possible conditions.
WHY IT MATTERS
While audits are expert review, formal verification is mathematical proof. Using tools like Certora Prover, developers write specifications (invariants and properties) and the tool mathematically proves the code satisfies them — or provides counterexamples showing where it doesn't.
Formal verification can prove statements like: 'total deposits always equal total withdrawals plus current balance' or 'no user can withdraw more than they deposited.' These proofs hold for ALL possible inputs and states, not just tested ones.
The limitation: formal verification proves code matches specification. If the specification is wrong, the verification is meaningless. It also can't catch economic/game-theoretic attacks that aren't expressible in the formal model.