Formal Verification of Contracts

In 2023, DeFi protocols lost over $1.8 billion due to smart contract vulnerabilities. Tests covered all known scenarios, auditors reviewed code line by line, and hacks happened anyway. The problem is that testing checks a finite number of cases, while an attacker searches for the one that was missed. Formal verification changes the rules: instead of checking a thousand inputs, it mathematically proves that a property holds for ALL possible inputs. This is not testing with better coverage. It's a mathematical proof of correctness.

• **Aave V3** - the largest lending protocol ($10B+ TVL) uses Certora for formal verification of all core contracts. Over 200 CVL rules verify: correctness of liquidations, accounting integrity, and the impossibility of withdrawing others' funds. The specifications are published as open source
• **Compound V3 (Comet)** - underwent formal verification via Certora with 80+ rules and invariants before launch. Each protocol update is re-verified. Result: zero critical incidents since launch
• **Uniswap V2** - Runtime Verification (creators of K Framework) formally proved via KEVM the correctness of the AMM x*y=k formula: a swap always preserves the invariant, and liquidity providers don't lose funds when used correctly

Предварительные знания

• Reentrancy and Classic Attacks

Symbolic Execution: Running a Program with Variables Instead of Values

Regular testing checks a contract against specific inputs: "if a user deposited 1 ETH, can they withdraw 2?" But the space of possible inputs is infinite. **Symbolic execution** flips the approach: instead of concrete values, **symbols** (α, β, γ) are substituted into variables, and the program is executed across all possible paths simultaneously. At every branch (`if`, `require`), the path splits, and each branch accumulates a set of **constraints** on the symbols. If even one path leads to an invariant violation - the tool has found a bug.

Main symbolic execution tools for smart contracts: **Mythril** (ConsenSys) - analyzes EVM bytecode, finds reentrancy, integer overflow, selfdestruct. **Manticore** (Trail of Bits) - symbolic execution with a Python API for writing custom detectors. **HEVM** (dapptools/Foundry) - symbolic execution directly from Foundry tests using `vm.assume()` and cheatcodes.

The main problem with symbolic execution is **path explosion**. Every `if` doubles the number of paths; a `for(i=0; i<n; i++)` loop creates n paths. A contract with 30 nested branches has 2^30 ≈ 1 billion paths. The solution is **bounded model checking**: limit the depth of analysis (e.g., to 3 transactions or 128 loop iterations). This is a trade-off: we don't check all possible paths, but we find bugs in reasonable time.

SMT Solvers: The Mathematical Engine of Verification

Symbolic execution collects constraints like `β >= α ∧ α > 0 ∧ β < 2^256`. But who decides whether values α and β satisfying these constraints actually exist? That's the job of **SMT solvers** (Satisfiability Modulo Theories) - programs that answer the question: "Does a set of values exist for which this formula is true?" SAT solvers work with boolean formulas (true/false), while SMT extends them with **theories** - integer arithmetic, bit vectors, and arrays. For the EVM, the theory of **bit vectors** is especially important, because uint256 is exactly a 256-bit vector with modular arithmetic.

Starting from version 0.8.4, Solidity has a **built-in SMTChecker** - a formal verifier right in the compiler. It uses Z3 or Eldarica and checks: underflow/overflow, division by zero, assertions, out-of-bounds array access, and unreachable code. Activated via `pragma experimental SMTChecker;` or the `solc --model-checker-engine all` option. This is the most accessible formal verification tool - no separate installation needed.

SMT solvers have a fundamental limitation: for some theories, the problem is **undecidable**. Non-linear arithmetic (`a * b > c * d` where all are variables), recursive data structures, and infinite loops may result in `unknown` instead of `sat`/`unsat`. In practice this means the solver may run for minutes, hours, or never terminate. Formal verification tools set **timeouts** and depth limits - completeness is sacrificed for practicality.

Certora Prover: Industrial Verification of DeFi Protocols

Mythril and SMTChecker look for **known bug classes** (overflow, reentrancy). But how do you prove that a token's `totalSupply` **always** equals the sum of all balances? Or that no user can withdraw more than they deposited? For that, you need to formulate **custom properties** - and that's where **Certora Prover** begins. Certora uses the **CVL** (Certora Verification Language) specification language to describe rules, invariants, and properties that an SMT solver verifies against the contract's EVM bytecode. Aave, Compound, MakerDAO, Lido, and dozens of other protocols use Certora for formal verification before deployment.

Certora works as a cloud service: `certoraRun Token.sol --verify Token:Token.spec`. The prover takes from 5 minutes to several hours depending on contract and specification complexity. Results are available in a web interface with counterexample visualization. Certora offers a free tier for open-source projects and actively collaborates with auditing firms.

Formal verification via Certora **does not guarantee** the absence of all bugs. It proves that the contract conforms to the **specification** - but the specification itself may be incomplete or incorrect. If you forgot to describe a property, Certora won't check it. Additionally, Certora does not analyze: economic attacks (flash loans, MEV), configuration errors (wrong addresses, privileges), or infrastructure-level issues (private key leaks, oracle manipulation). Formal verification is a powerful tool, but it's just one layer in defense in depth.

K Framework: Formal Semantics of the EVM

Certora proves contract properties by interpreting its bytecode. But how accurate is that interpretation? What if the **verification tool itself** misunderstands how the EVM works? **K Framework** addresses this radically: instead of interpreting bytecode, it creates a **formal mathematical semantics** of the EVM - a complete description of every opcode, every gas calculation rule, every edge case. This is the **KEVM** (K Ethereum Virtual Machine) project, developed by **Runtime Verification**. With a formal semantics, properties of contracts can be proven with mathematical rigor, where every EVM step is defined unambiguously.

The most famous K Framework verification project is **Uniswap V2**. Runtime Verification formally proved correctness of the AMM's key properties: the `x * y = k` formula is preserved after every swap, liquidity providers don't lose funds when used correctly, and swap operations always execute at the stated price. Other projects: **Gnosis Safe** (multisig wallet), **Ethereum 2.0 deposit contract**, **ERC-20** reference implementation.

In practice, tool selection depends on project requirements. For most DeFi protocols, **Certora** is the optimal choice: approachable language, cloud infrastructure, results in minutes. **K Framework** is used for critical infrastructure requiring absolute mathematical rigor: core protocols (Uniswap, Gnosis), bridges, Ethereum system contracts. Neither tool replaces auditing and testing - they complement them, forming yet another layer of defense in depth.

Key Takeaways

• **Symbolic execution** runs a program with symbols instead of concrete values, exploring all paths simultaneously. At each branch, paths split and constraints accumulate. Path explosion is the main enemy, addressed through bounded model checking
• **SMT solvers** (Z3, Bitwuzla) are the mathematical engines solving constraint systems from symbolic execution. The bitvector theory is critical for the EVM (uint256 = 256-bit bitvector). Solidity's SMTChecker uses Z3 directly in the compiler
• **Certora Prover** lets you describe custom properties in CVL: invariants (`totalSupply == Σ balances`), rules (transfer doesn't change totalSupply), and parametric rules (no function decreases another user's balance). Ghost variables and hooks connect the specification to the contract's storage
• **K Framework / KEVM** - formal semantics of the EVM: a mathematical definition of each of the 140+ opcodes. Unlike Certora (property-based), K Framework verifies through a precise EVM model, eliminating abstraction errors. Used for critical infrastructure (Uniswap, Gnosis Safe)
• No single tool replaces all others. DeFi protocols lost $1.8B in a year despite testing and audits - formal verification adds mathematical rigor but only checks what's described in the specification. **Defense in depth**: SMTChecker → Mythril → Certora → audit → fuzzing → monitoring

Related Topics

Formal verification is one layer of smart contract security, closely tied to other protective methods:

• Reentrancy and Classic Attacks — Symbolic execution tools like Mythril automatically detect reentrancy patterns. Certora allows proving the absence of reentrancy through invariants on state transitions
• Security: Overflow and Underflow — SMT solvers are ideal for finding integer overflow - Z3 solves the question 'can a uint256 overflow' in milliseconds. Solidity's SMTChecker finds overflow at compile time
• Smart Contract Fuzzing — Fuzzing (Echidna, Foundry) and formal verification are complementary approaches: fuzzing finds bugs quickly, while verification mathematically proves the absence of entire classes of bugs. The best protocols use both
• Security Auditing — Formal verification doesn't replace manual auditing: economic attacks, governance vulnerabilities, and architectural issues require human analysis. Verification + audit = defense in depth

Вопросы для размышления

• A Certora specification for an ERC-20 token contains 50 rules and all show VERIFIED. Does this mean the token cannot be hacked? What types of attacks remain beyond even a perfect CVL specification?
• K Framework provides academic rigor but requires months of work and rare specialists. Certora is easier to use but depends on an EVM abstraction. For a startup with $5M TVL and a limited budget - what level of formal verification is justified? Can you get by with just SMTChecker and Mythril?
• Formal verification of Compound V3 cost hundreds of thousands of dollars and took months. Meanwhile, one developer with Foundry can write an extensive fuzzing campaign in a week. From a security ROI standpoint - when does formal verification justify its cost, and when is fuzzing enough?

Связанные уроки

• fl-33-formal-verification