Glossary
Formal Verification
Mathematically proving — not just testing — that a smart contract satisfies a precise specification, using tools like Certora, K, or proof assistants.
Formal verification replaces testing with proof. The engineer writes a specification ("the total supply equals the sum of balances", "no caller can drain more than their balance") and a verification tool either proves the spec holds for every possible input or produces a counterexample.
Tools like Certora Prover, Halmos, KEVM, and dedicated proof assistants (Coq, Lean, Isabelle) are used on the most safety-critical contracts: Maker, Aave, Compound, Lido. The cost is steep — writing the spec correctly is its own engineering effort — but for billion- dollar contracts, it is increasingly the standard.