Formal Verification of Smart Contracts

Formal Verification of Smart Contracts

Formal verification is a mathematical proof of program correctness. Not "we checked all test cases," but "we proved that for any input data the contract behaves according to specification." The difference is critical: tests find presence of errors, verification proves their absence. MakerDAO, Aave, Compound use formal verification for critical components. Let's examine how it works in practice.

Formal Verification Tools

Certora Prover

Certora Prover — the most common tool for EVM smart contracts. Uses its own specification language CVL (Certora Verification Language). Works as SaaS — upload contract and specification, get results.

Specifications are written in CVL:

// Specification for ERC-20 transfer
methods {
    function transfer(address, uint256) external returns (bool) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function totalSupply() external returns (uint256) envfree;
}

// Invariant: sum of all balances = totalSupply
invariant totalSupplyIsSum(address a, address b)
    a != b =>
    balanceOf(a) + balanceOf(b) <= totalSupply();

// Rule: transfer decreases sender balance
rule transferDecreasesBalance(address sender, address recipient, uint256 amount) {
    require sender != recipient;
    require balanceOf(sender) >= amount;

    uint256 balanceBefore = balanceOf(sender);

    env e;
    require e.msg.sender == sender;
    transfer(e, recipient, amount);

    assert balanceOf(sender) == balanceBefore - amount;
}

// Rule: transfer never creates tokens from thin air
rule noTokenCreation(method f, address a) {
    uint256 totalBefore = totalSupply();

    env e;
    calldataarg args;
    f(e, args);

    assert totalSupply() <= totalBefore;
}

Prover attempts to find counterexample — set of inputs where assertion is violated. If counterexample not found in given time — specification considered proven.

Solidity SMTChecker

Built into Solidity compiler, based on SMT (Satisfiability Modulo Theories). Activated through pragma or compiler flags:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
// Enable SMT checking
/// @custom:smtchecker abstract-function-nondet

contract VaultVerified {
    mapping(address => uint256) public balances;
    uint256 public totalDeposited;

    function deposit(uint256 amount) external {
        require(amount > 0, "Zero amount");

        // SMTChecker automatically verifies:
        // - no overflow in balances[msg.sender] += amount
        // - no overflow in totalDeposited += amount
        // - invariant: totalDeposited = Σ balances[i]

        balances[msg.sender] += amount;
        totalDeposited += amount;
    }

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

        balances[msg.sender] -= amount;
        totalDeposited -= amount;
        // assert not needed — SMTChecker verifies underflow impossible
    }
}

Run through Hardhat:

npx hardhat compile --config hardhat.smtchecker.config.ts

// hardhat.smtchecker.config.ts
export default {
    solidity: {
        version: "0.8.20",
        settings: {
            modelChecker: {
                engine: "chc",        // Constrained Horn Clauses — most powerful
                targets: [
                    "assert",
                    "overflow",
                    "underflow",
                    "divByZero",
                    "constantCondition",
                    "balance"
                ],
                timeout: 20000,       // milliseconds per check
                showUnproved: true
            }
        }
    }
};

Halmos

Halmos — symbolic execution for EVM, written in Python. Works with existing Foundry tests — symbolically executes them for all possible inputs:

// Foundry test becomes formal verification in Halmos
// Run: halmos --contract TestVault --function testFormal

contract TestVault is Test {
    Vault vault;

    function setUp() public {
        vault = new Vault(address(token));
    }

    // Halmos runs this for ALL possible values of amount and caller
    function testFormal_depositWithdraw(
        uint256 amount,
        address caller
    ) public {
        vm.assume(amount > 0 && amount < type(uint128).max);
        vm.assume(caller != address(0));

        deal(address(token), caller, amount);

        vm.prank(caller);
        token.approve(address(vault), amount);

        vm.prank(caller);
        vault.deposit(amount);

        uint256 shares = vault.balanceOf(caller);

        vm.prank(caller);
        vault.withdraw(shares);

        // For all possible amount and caller: after deposit+withdraw
        // balance recovers (accounting for fees)
        assertGe(token.balanceOf(caller), amount * 99 / 100);
    }
}

Specification: The Most Difficult Part

Tools are means. Main work is writing specification. Bad specification proves contract correct according to wrong requirements.

Types of Properties for Verification

Safety properties ("bad never happens"):

• Balance never goes negative
• totalSupply never exceeds MAX_SUPPLY
• Only owner can call pause()
• Reentrancy guard works correctly

Liveness properties ("good eventually happens"):

• If user deposits funds, they can withdraw them
• Proposals eventually execute or reject
• Staker eventually receives rewards

Invariants ("always true"):

• Σ balances = totalSupply (conservation of tokens)
• lockedAmount <= totalDeposited
• Oracle price always > 0

Example Complete Specification for Lending Protocol

// Specification for simplified Aave-like protocol

methods {
    function deposit(uint256) external envfree;
    function borrow(uint256) external envfree;
    function repay(uint256) external envfree;
    function liquidate(address) external;
    function getHealthFactor(address) external returns (uint256) envfree;
    function collateral(address) external returns (uint256) envfree;
    function debt(address) external returns (uint256) envfree;
}

// Invariant: cannot liquidate healthy borrower
rule noLiquidationOfHealthyBorrower(address borrower) {
    require getHealthFactor(borrower) >= 1e18; // health factor >= 1.0

    env e;
    liquidate@withrevert(e, borrower);

    assert lastReverted, "Healthy borrower should not be liquidatable";
}

// Invariant: sum of debts doesn't exceed sum of collateral (with LTV coefficient)
invariant solvencyInvariant(address user)
    debt(user) * 100 <= collateral(user) * MAX_LTV_PERCENT
    filtered { f -> !f.isView }

// Reentrancy: state cannot change twice in one transaction
rule noReentrancy(method f) {
    uint256 collateralBefore = collateral(currentContract);

    env e;
    calldataarg args;
    f(e, args);

    uint256 collateralAfter = collateral(currentContract);

    // Balance changed exactly as expected
    assert collateralAfter >= collateralBefore || /* withdrawal */
           collateralAfter <= collateralBefore; // deposit
}

Limitations of Formal Verification

Formal verification is not a silver bullet:

Completeness gap: only what's specified in specification is verified. If attacker finds vector not covered by specification — verification won't catch it. This happened with some "verified" protocols.

Scalability: large contracts (> 1000 lines) are difficult to verify completely. Tools may not finish in reasonable time (timeout). Solution — verify critical components separately.

Oracle assumptions: if contract uses oracle, verification assumes oracle returns correct data. Incorrect oracle — outside verification scope.

External calls: interaction with external contracts is difficult to specify completely. Certora requires explicit specification of external behavior through summarization.

Verification Audit Process

Full formal verification process:

Stage 1 — Requirements Specification: jointly with protocol team define critical properties that must hold under any conditions.

Stage 2 — CVL/Halmos Specification Writing: 2-4 weeks for typical DeFi protocol. Cover safety invariants, access control, economic invariants.

Stage 3 — Iterative Verification: run Prover, analyze counterexamples, refine specification or fix code. This is iterative process.

Stage 4 — Report: list of verified properties, found violations, verification limitations.

Typical cost of verification audit — $50k-$200k depending on protocol complexity. Significantly more than usual audit, but justified for contracts with $100M+ TVL: cost of finding one critical vulnerability worth $10k in specification can prevent $10M loss.

Formal verification does not replace manual audit — they complement each other. Manual audit finds logic errors in business logic, verification proves correctness of mathematical properties.