A Practical Guide to Formal Verification for Smart Contracts
HasFocus Research · 2025
Abstract
Formal verification provides mathematical guarantees that specified properties hold for all possible inputs. This guide introduces the concept, surveys available tools (Certora, Halmos, HEVM), and provides practical advice on what properties to verify in DeFi protocols.
1. What Is Formal Verification?
Unlike testing (which checks specific inputs), formal verification mathematically proves that a property holds for ALL possible inputs and states. For smart contracts, this means proving that invariants like 'total supply equals sum of all balances' hold regardless of the sequence of transactions. This is especially valuable for protocols holding significant value.
2. Available Tools
Several tools are available for Solidity formal verification. Certora Prover operates on compiled bytecode and uses its own specification language (CVL). Halmos uses symbolic execution with Python-based property definitions. HEVM provides symbolic execution integrated with Foundry. Each has tradeoffs in expressiveness, performance, and learning curve.
3. What to Verify
Start with high-value invariants: token supply conservation, no-profit-from-self-interaction, monotonicity of share prices, and solvency (total assets >= total liabilities). For AMMs, verify the constant-product invariant. For lending protocols, verify that liquidations always improve the health factor. For governance, verify that only valid proposals can be executed.
Want our team to review your protocol?
Our auditors apply this knowledge to protect real-world protocols every day.
Request an Audit