formal-verification

Formal Verification for Solidity

Tools

Tool	Approach	Strengths
Certora Prover	CVL specs + SMT solving	Industry standard, deep analysis
Halmos	Symbolic Foundry tests	Familiar Foundry interface, open source
KEVM	K Framework semantics	EVM bytecode level verification

Certora CVL Specification Template

// spec/Vault.spec

using ERC20 as token;

methods {
    function deposit(uint256) external returns (uint256);
    function withdraw(uint256, address, address) external returns (uint256);
    function totalAssets() external returns (uint256) envfree;
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function asset() external returns (address) envfree;

    // Summarize external calls
    function _.transfer(address, uint256) external => DISPATCHER(true);
    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
    function _.balanceOf(address) external => DISPATCHER(true);
}

Rule Types

Parametric Rules

Verify properties for all possible inputs:

// Depositing should increase total supply
rule depositIncreasesSupply(uint256 assets) {
    env e;
    uint256 supplyBefore = totalSupply();

    deposit(e, assets);

    uint256 supplyAfter = totalSupply();
    assert supplyAfter >= supplyBefore, "supply must not decrease on deposit";
}

Invariant Rules

Properties that must hold in every reachable state:

// Solvency: vault always has enough assets to back shares
invariant solvency()
    totalSupply() == 0 || totalAssets() > 0
    {
        preserved deposit(uint256 assets) with (env e) {
            require assets > 0;
        }
    }

Relational Rules

Compare two executions:

// Monotonicity: depositing more gives more shares
rule depositMonotonicity(uint256 assets1, uint256 assets2) {
    env e;
    require assets1 < assets2;

    storage init = lastStorage;

    uint256 shares1 = deposit(e, assets1);

    uint256 shares2 = deposit(e, assets2) at init;

    assert shares2 >= shares1, "more assets should give more shares";
}