Deep Dive — Formal Verification

Why formal verification

Unit tests and fuzzing sample the input space. Formal verification reasons about it. The win:

• A unit test that passes on 1000 inputs proves nothing about input 1001.
• An invariant proven by an SMT solver proves the property holds for all reachable states under the rule's assumptions.
• For protocol-critical properties — "no bad debt," "shares conserved across deposits/withdraws," "rate bounded" — that's the difference between "we tested" and "we proved."

FV doesn't replace audits, fuzzing, or testing. It's the highest tier of a defense-in-depth pyramid. Most senior security engineers spend 30-60% of their week here.

Certora and CVL

Certora is a commercial SaaS formal verification product. You write specifications in CVL (Certora Verification Language), upload them with the source, and Certora's Prover lowers everything to SMT (typically z3 or cvc5) and either:

1. Proves the property holds on all paths (✓), or
2. Returns a counterexample — a sequence of calls that violates it, or
3. Times out / returns "unknown" — the solver couldn't decide within the budget.

The product also includes a hosted run interface (the "Prover Dashboard") where you see verification reports, call traces for counterexamples, and the SMT model. Pricing is commercial; most serious DeFi teams have a license.

CVL syntax that matters

CVL syntax echoes Solidity but is its own DSL. The core constructs:

Rules

rule depositIncreasesShares(uint256 assets, address receiver) {
    env e;
    require receiver != 0;
    uint256 sharesBefore = balanceOf(receiver);
    uint256 shares = deposit(e, assets, receiver);
    uint256 sharesAfter = balanceOf(receiver);
    assert sharesAfter == sharesBefore + shares;
}

A rule is a single property that should hold after one method call. CVL checks it on every public function unless you scope.

Parametric rules

One of the most powerful idioms — quantify over all public methods:

rule onlyOwnerCanPause(method f, env e, calldataarg args) {
    require !paused();
    f(e, args);
    assert paused() => e.msg.sender == owner();
}

Certora explodes f across every public function, so a single rule like this checks the entire access-control surface.

Invariants

Invariants are properties that hold in every reachable state. CVL proves them inductively — true at construction, preserved by every function.

invariant totalSupplyEqualsSumOfBalances()
    totalSupply() == sumOfBalances()
    {
        preserved transfer(address to, uint256 amount) with (env e) {
            require balanceOf(e.msg.sender) >= amount;
        }
    }

Definitions and functions

definition declares a reusable predicate. function declares helper code (in CVL or via summarization of Solidity).

definition isInitialized(address market) returns bool =
    lastUpdate(market) != 0;

function setupHealthyMarket(address m) {
    require isInitialized(m);
    require totalSupplyAssets(m) >= totalBorrowAssets(m);
}

Ghost variables and hooks

Ghost state is invisible to the contract but tracked by the Prover. Used to express properties that aren't directly visible in storage — sums, counts, "this thing happened" flags.

ghost mathint sumBalances {
    init_state axiom sumBalances == 0;
}

hook Sstore _balances[KEY address k] uint256 newVal (uint256 oldVal) STORAGE {
    sumBalances = sumBalances + newVal - oldVal;
}

invariant totalSupplyEqSumBalances()
    totalSupply() == sumBalances;

Hooks fire on storage reads/writes, function entry/exit, opcodes. They're how you keep ghost state in sync. They're also the part of CVL that takes the longest to internalize.

The SMT solver model

What the Prover actually does under the hood:

1. Symbolically execute every path through the function.
2. Encode the program semantics + your assertion as an SMT formula in (typically) the theory of arrays, bitvectors, and uninterpreted functions.
3. Negate the assertion; ask the solver "is there a model where the program runs and the property fails?"
4. If UNSAT — the property holds. If SAT — the model is your counterexample. If timeout — solver gave up.

Practical consequences:

• Nonlinear arithmetic (multiplication, division of two symbolic values) is hard for solvers. You'll see timeouts.
• Loops are unrolled or summarized. Unbounded loops require a loop_iter setting.
• External calls are summarized — you give the Prover a model of what they return.
• Storage is modeled as an array with uninterpreted keys. Mappings work fine; complex nested encodings can confuse the solver.

Managing state explosion

The single most common reason CVL specs time out: the model has too many paths or too much symbolic state. The standard moves to control it:

Linking

Tell the Prover which deployed contract address corresponds to which Solidity contract type. Without linking, an external call to IERC20(token).balanceOf(x) is fully symbolic — the solver has to consider every possible token contract.

using ERC20 as token;
methods {
    function token.balanceOf(address) external returns uint256 envfree;
}

Summarization

Replace a complex function with a simpler model the solver can handle.

methods {
    function _._convertToShares(uint256 a, MathRoundingLib.Rounding r) internal
        returns (uint256) => CVLConvertToShares(a, r);
}

function CVLConvertToShares(uint256 a, MathRoundingLib.Rounding r) returns uint256 {
    uint256 result;
    require result <= a; // approximate but sound for our property
    return result;
}

Summaries trade fidelity for tractability. The risk: an over-loose summary lets bugs through; an over-tight one makes the spec vacuous. This is a craft skill.

requireInvariant

Carry a proven invariant into a new rule as an assumption, so you're not re-proving global facts inside every rule.

Splitting

If a parametric rule times out on one method, scope it: filtered { f -> f.selector != sig:harderFunction().selector } and prove that one separately with a different config.

When FV wins, when it doesn't

Wins:

• Core conservation laws. "Total supply = sum of balances." "No bad debt." "Position health monotonic in collateral."
• Access control. "Only the role-X address can call function Y."
• Math invariants. "Shares-to-assets rounding always favors the protocol."
• Upgrade safety. "Storage layout unchanged across upgrade."

Doesn't win (cleanly):

• Economic / game-theoretic properties. "An attacker can't profitably manipulate the oracle." Solver can't reason about external markets.
• Cross-protocol composition. If your protocol composes with three others, you can't model all of them.
• Gas-related properties. Solver doesn't reason about gas.
• MEV. Out of model.

The economic things still need adversarial review and incident-response design. FV is one pillar, not the building.

The first 20 invariants you'd write for a lending market

A common interview prompt: "you arrive at a lending protocol with no FV. What do you spec first?" A defensible list:

1. Total borrow shares = sum of user borrow shares.
2. Total supply shares = sum of user supply shares.
3. Total borrow assets ≤ total supply assets (no bad debt).
4. Conversion: shares-to-assets rounds down on user-favoring operations, up on protocol-favoring.
5. A user's borrow position has a non-zero collateral.
6. After borrow, the user is healthy (collateral × LTV ≥ debt).
7. Liquidation reduces total debt.
8. Liquidation cannot increase a user's health below threshold (no over-liquidation).
9. Interest rate monotonic in utilization.
10. Interest accrual is monotonic in time (rate ≥ 0 always).
11. Cumulative borrow index only increases.
12. Only owner / role X can change market parameters.
13. Initialized markets cannot be re-initialized.
14. Paused markets reject deposits / borrows.
15. Total assets in vault = idle + sum of supplied across markets.
16. Withdraw cannot increase the caller's borrow.
17. Repay decreases the caller's borrow by at most the principal owed.
18. Liquidation bonus paid ≤ configured cap.
19. Oracle staleness check rejects updates older than threshold.
20. Re-entrancy lock prevents nested calls on state-modifying entries.

Halmos — symbolic execution of Foundry tests

Halmos is an open-source symbolic execution engine from a16z. The pitch: write Foundry tests as usual, but the runner replaces concrete inputs with symbolic ones and explores all paths.

// In a Foundry test
function check_NoBadDebt(uint256 amount, address user) public {
    vm.assume(amount > 0);
    vm.assume(user != address(0));
    market.deposit(amount, user);
    uint256 totalBorrow = market.totalBorrowAssets();
    uint256 totalSupply = market.totalSupplyAssets();
    assert(totalBorrow <= totalSupply);
}

halmos --function check_NoBadDebt

Advantages: no separate spec language; tests are portable; free. Limitations: less mature than Certora at non-linear math, summarization, and complex codebases. Halmos shines on small, well-scoped properties.

Kontrol — K-framework based

Kontrol (from Runtime Verification) builds on the K framework — a semantics-engineering platform that gives you an executable model of the EVM. The pitch: you can prove properties at the EVM bytecode level, which catches compiler bugs and inline-assembly mistakes that source-level tools miss.

Used heavily on protocols where Yul / inline-assembly is load-bearing (e.g., some optimizers, custom precompile-like contracts). Steeper learning curve than CVL; smaller community; high ceiling.

Tradeoffs between tools