formal verification

Formal verification proves mathematically that a contract satisfies a specified property for every possible input and execution path, rather than checking a handful of hand-picked examples and hoping the rest behave. Testing can only show the presence of bugs on the cases you tried; formal verification aims to show their absence with respect to a precise specification. You write down what must always be true, and a tool either produces a proof that it holds or a concrete counterexample, a sequence of calls that breaks it.

Mechanically, the property is encoded as a formal specification, often an invariant such as the total token supply always equals the sum of all balances, or a postcondition relating a function's inputs to its outputs. A verification engine then explores the program's behavior symbolically rather than concretely: it reasons about the contract over symbolic values using SMT solvers, theorem provers, or symbolic execution, covering all paths at once. Tools in this space include the Certora Prover with its CVL specification language, Solidity's built-in SMTChecker, Halmos, the K framework, and symbolic-execution engines such as Manticore.

Formal verification is the strongest assurance available, but its power is bounded by what you specify. It proves only the properties you actually wrote down, so a correct proof of an incomplete or wrong specification gives false confidence. The hard, expensive work is choosing the right invariants and modeling the environment faithfully; on top of that, solvers can time out on complex code and unbounded loops resist full proof. It is best used to lock down the most critical invariants of high-value contracts, alongside, not instead of, auditing and fuzzing.