Testing tells you what your code does in specific scenarios. Formal verification tells you what your code does in all scenarios. When a single edge case can drain millions, that difference matters.

In 2016, The DAO was “tested”—but testing didn’t catch the reentrancy bug that led to a $60M loss and Ethereum’s controversial hard fork. Could formal verification have prevented it? In many cases, yes.

What Is Formal Verification?

Formal verification uses mathematical proofs to verify that code behaves according to its specification. Instead of running tests with example inputs, it exhaustively analyzes all possible execution paths.

Think of it this way:

• Testing: “I tried 10,000 inputs and they all worked”
• Formal Verification: “I mathematically proved this works for all possible inputs”

The catch? You need to define what “works” means. Formal verification proves your code matches your specification—if your specification is wrong, the proof is useless.

Types of Formal Verification

Symbolic Execution

Treats inputs as symbols rather than concrete values, exploring all possible paths through the code.

Tools: Mythril, Manticore

function withdraw(uint256 amount) external {
    require(balances[msg.sender] >= amount, "Insufficient");
    balances[msg.sender] -= amount;
    payable(msg.sender).transfer(amount);
}

Symbolic execution would analyze this with amount as a symbol representing any possible value, checking every path:

• What if amount is 0?
• What if amount equals the exact balance?
• What if the subtraction would underflow (caught by Solidity 0.8+)?
• What if the transfer fails?

Model Checking

Verifies that a finite-state model of your system satisfies certain properties.

Tools: Certora Prover, KEVM

You define invariants (properties that must always hold), and the model checker exhaustively verifies them:

// Certora specification
invariant totalSupplyMatchesSum()
    sumOfBalances() == totalSupply()

Theorem Proving

The most rigorous approach. Uses mathematical logic to construct proofs about code behavior.

Tools: Coq, Isabelle, Lean

This requires writing code in a proof-friendly language or translating to one. It’s the gold standard but extremely labor-intensive.

Practical Formal Verification with Foundry

Foundry’s invariant testing brings formal verification concepts to everyday development without specialized tools.

Invariant Testing Basics

Define properties that must hold across random sequences of function calls:

// Target contract
contract Vault {
    mapping(address => uint256) public balances;
    uint256 public totalDeposited;

    function deposit() external payable {
        balances[msg.sender] += msg.value;
        totalDeposited += msg.value;
    }

    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "Insufficient");
        balances[msg.sender] -= amount;
        totalDeposited -= amount;
        payable(msg.sender).transfer(amount);
    }
}

// Invariant test
contract VaultInvariantTest is Test {
    Vault vault;

    function setUp() public {
        vault = new Vault();
        // Fund test accounts
        targetContract(address(vault));
    }

    // This invariant is checked after every random call sequence
    function invariant_totalMatchesBalance() public {
        assertEq(
            address(vault).balance,
            vault.totalDeposited(),
            "Balance mismatch"
        );
    }

    function invariant_noNegativeBalances() public {
        // Implicitly true due to uint256, but documents intent
    }
}

Run with forge test --mt invariant and Foundry will:

1. Generate random call sequences
2. Execute them against your contract
3. Check invariants after each sequence
4. Report any violations with the exact call sequence

Handler Contracts for Complex Scenarios

For protocols with multiple contracts and complex interactions, use handlers:

contract VaultHandler is Test {
    Vault vault;
    address[] actors;

    constructor(Vault _vault) {
        vault = _vault;
        // Create test actors
        for (uint i = 0; i < 10; i++) {
            actors.push(makeAddr(string.concat("actor", vm.toString(i))));
            deal(actors[i], 100 ether);
        }
    }

    function deposit(uint256 actorSeed, uint256 amount) external {
        address actor = actors[actorSeed % actors.length];
        amount = bound(amount, 0, actor.balance);

        vm.prank(actor);
        vault.deposit{value: amount}();
    }

    function withdraw(uint256 actorSeed, uint256 amount) external {
        address actor = actors[actorSeed % actors.length];
        amount = bound(amount, 0, vault.balances(actor));

        vm.prank(actor);
        vault.withdraw(amount);
    }
}

Certora: Industrial-Strength Verification

Certora Prover is the most widely used formal verification tool in DeFi. It’s been used by Aave, Compound, Maker, and dozens of major protocols.

Writing Certora Specifications

Specifications are written in CVL (Certora Verification Language):

// spec/Vault.spec

methods {
    function balances(address) external returns (uint256) envfree;
    function totalDeposited() external returns (uint256) envfree;
    function deposit() external;
    function withdraw(uint256) external;
}

// Invariant: sum of all balances equals totalDeposited
ghost mathint sumBalances {
    init_state axiom sumBalances == 0;
}

hook Sstore balances[KEY address user] uint256 newBalance (uint256 oldBalance) {
    sumBalances = sumBalances + newBalance - oldBalance;
}

invariant sumMatchesTotal()
    sumBalances == to_mathint(totalDeposited())

// Rule: deposit increases balance correctly
rule depositIncreasesBalance(env e) {
    uint256 balanceBefore = balances(e.msg.sender);
    uint256 totalBefore = totalDeposited();
    uint256 depositAmount = e.msg.value;

    deposit(e);

    uint256 balanceAfter = balances(e.msg.sender);
    uint256 totalAfter = totalDeposited();

    assert balanceAfter == balanceBefore + depositAmount;
    assert totalAfter == totalBefore + depositAmount;
}

// Rule: withdraw decreases balance correctly
rule withdrawDecreasesBalance(env e, uint256 amount) {
    uint256 balanceBefore = balances(e.msg.sender);
    require balanceBefore >= amount; // Precondition

    withdraw(e, amount);

    uint256 balanceAfter = balances(e.msg.sender);
    assert balanceAfter == balanceBefore - amount;
}

// Rule: no user can withdraw more than their balance
rule noOverWithdraw(env e, uint256 amount) {
    uint256 balance = balances(e.msg.sender);

    withdraw@withrevert(e, amount);

    assert amount > balance => lastReverted;
}

Running Certora

certoraRun contracts/Vault.sol:Vault 
    --verify Vault:spec/Vault.spec 
    --solc solc8.19

Certora will either:

• Prove all rules hold for all possible inputs
• Provide a counterexample showing exactly how a rule can be violated

When to Use Formal Verification

High-Value Targets

If your contract will hold significant value, formal verification is likely worth it:

• Core DeFi primitives (lending pools, AMMs)
• Bridge contracts
• Protocol treasuries
• Staking/reward mechanisms

Complex Mathematical Logic

When correctness depends on mathematical properties:

• Interest rate calculations
• Share/asset conversions
• Price calculations
• Bonding curves

Critical Invariants

When certain properties absolutely must hold:

• Conservation of funds (no money created/destroyed)
• Access control correctness
• State transition validity

Not Worth It For

• Simple getter functions
• UI contracts with minimal logic
• Contracts with well-understood patterns and no custom logic
• Prototypes and MVPs (focus on design first)

Limitations of Formal Verification

Specification Errors

Formal verification proves code matches spec. If your spec is wrong, the proof is meaningless.

// Wrong spec: accidentally allows draining
rule withdrawCorrect(env e, uint256 amount) {
    // Forgot to require amount <= balance
    withdraw(e, amount);
    assert true; // This proves nothing useful
}

External Dependencies

Formal verification typically assumes external calls behave as specified. If you integrate with a malicious contract, proofs don’t help.

Gas and Execution Environment

Most formal verification tools abstract away gas costs and low-level EVM behavior. Bugs caused by gas manipulation or EVM quirks may not be caught.

Complexity Limitations

Some properties are computationally infeasible to verify. Tools may timeout on very complex contracts or require simplifications that reduce coverage.

Integrating Formal Verification into Development

Start with Invariant Testing

Before investing in Certora or other tools, establish invariants with Foundry:

// Cheap to write, catches many bugs
function invariant_conservationOfValue() public {
    assertEq(
        token.totalSupply(),
        sumOfAllBalances()
    );
}

Define Critical Properties Early

Document invariants during design, not after implementation:

## Protocol Invariants

1. Total supply always equals sum of all balances
2. No address can withdraw more than deposited
3. Only authorized roles can call admin functions
4. Share price can never decrease due to user actions

Progressive Verification

Start with the most critical properties and expand:

1. Week 1: Core value conservation
2. Week 2: Access control correctness
3. Week 3: Economic invariants (no arbitrage, fair distribution)
4. Week 4: Edge cases and complex scenarios

Combine with Other Methods

Formal verification is one tool in the security toolbox:

• Fuzzing: Quick, catches many bugs
• Static analysis: Low effort, high coverage
• Formal verification: High confidence for specific properties
• Manual audit: Catches logic errors and design flaws

Cost-Benefit Analysis

Time Investment

Approach	Initial Setup	Per-Property Time
Foundry Invariants	2-4 hours	30 min - 2 hours
Certora	1-2 days	4-8 hours
Theorem Proving	Weeks	Days-weeks

ROI Calculation

For a protocol holding $100M:

• Certora setup + core properties: ~$50,000 (including auditor time)
• Probability of catching critical bug: 10-20%
• Expected value of bug: $10M+ (10% of TVL)
• Expected savings: $1M - $2M

For most major protocols, formal verification has positive expected value.

Key Takeaways

1. Formal verification proves properties for all inputs—not just tested ones
2. Start with Foundry invariant testing—it’s free and catches many bugs
3. Certora is the industry standard—proven on billions of dollars of DeFi
4. Verification is only as good as specifications—invest in defining correct properties
5. Combine multiple approaches—no single method catches everything
6. Focus on high-value, high-risk code—not everything needs formal verification

Testing tells you “it worked for these cases.” Formal verification tells you “it works for all cases.” When the stakes are high enough, that certainty is worth the investment.

---

Interested in formal verification for your protocol? Get in touch to discuss whether it’s the right approach for your security needs.