Formal verification

Testing checks a contract against the cases someone thought to write; formal verification aims to cover all of them. Engineers first write a specification, a set of properties the code must always respect, such as total supply equals the sum of balances or no user can withdraw more than they deposited. Tools such as SMT solvers, symbolic execution engines or proof assistants then try to prove those properties hold for every input and state, or produce a counterexample.

Because contracts are immutable and hold large sums, high-value protocols increasingly pay for it. Ethereum's beacon chain deposit contract was formally verified before launch, and lending markets, stablecoins and DEXs use specialised provers to check core invariants. Rollups and ZK circuits are also natural candidates, since their correctness is mathematical by nature.

A proof is only as good as its specification: if the properties miss the real risk, verified code can still be exploited, and assumptions about external contracts, oracles or the compiler may not hold. The process is slow and expensive, so it is usually applied to the most critical components and combined with audits, fuzzing and bug bounties rather than replacing them.