Traditional security audits are still prone to human error - manual audits can miss edge cases, unit tests are only as good as the scenarios written, and test coverage does not guarantee the absence of logic bugs. Formal verification addresses this gap by checking every possible contract state and execution path to identify critical vulnerabilities that hackers can exploit.

In this article, we explore the process of formally verifying an ERC-4626 vault - a standardized tokenized yield-bearing vault - using Certora Prover. Certora is a powerful rule-based verification tool that allows developers to define custom correctness properties and enforce them on Solidity smart contracts, ensuring their security before deployment.

What Is Formal Verification?

Unlike traditional testing, which relies on specific inputs and outputs to verify contract behavior, formal verification enables mathematical reasoning over all possible states. It ensures that a smart contract adheres to its intended logic under all conditions, including edge cases that would be impractical to test manually.

Formal verification works by translating smart contract code and its desired properties into mathematical formulas. A prover engine then exhaustively checks whether these properties hold for every conceivable input and state combination. If a violation is found, the prover provides a concrete counterexample demonstrating the failure.

Key advantages of formal verification over traditional testing:

• Exhaustive coverage: Every possible execution path is analyzed, not just the ones a developer thinks to test
• Mathematical guarantees: Properties that pass verification are proven correct, not merely validated against a finite set of inputs
• Counterexample generation: When a property fails, the prover produces a specific scenario demonstrating the violation
• Invariant enforcement: Logical assertions about a contract's state that must remain true after every state transition can be verified across all operations

Understanding ERC-4626

ERC-4626 is a tokenized vault standard that provides a standardized API for yield-bearing vaults. It extends ERC-20 to represent shares of a vault, where users deposit an underlying asset token and receive share tokens representing their proportional ownership of the vault's total assets.

The standard defines key functions that any compliant vault must implement:

• deposit: Accept asset tokens and mint corresponding shares to the depositor
• withdraw: Burn shares and return the proportional amount of asset tokens
• mint: Mint a specific number of shares by depositing the required assets
• redeem: Redeem a specific number of shares for the underlying assets
• totalAssets: Return the total amount of underlying assets held by the vault
• convertToShares / convertToAssets: Preview conversion rates between assets and shares

The correctness of these functions is critical. A bug in the share calculation can lead to fund drainage, share dilution, or permanent loss of deposited assets. This makes ERC-4626 vaults an ideal candidate for formal verification.

Certora Prover Overview

Certora Prover is a formal verification tool designed specifically for smart contracts. It uses a specification language called CVL (Certora Verification Language) that allows developers to write rules, invariants, and properties that their contracts must satisfy.

The core workflow with Certora Prover involves three components:

1. The contract under test: The Solidity smart contract you want to verify
2. The spec file (.spec): A formal verification script defining rules and constraints
3. The configuration file (.conf): Specifies which contracts and specs to use during verification

A spec file serves as the blueprint for how the prover checks correctness. It specifies invariants, function behaviors, and assumptions about the contract's state. The prover then exhaustively checks whether all rules hold for every reachable state of the contract.

The Contract Under Test: VaultERC

The primary contract under test is VaultERC, which follows the ERC-4626 standard for tokenized vaults. It extends the base ERC4626 contract and overrides totalAssets() - a hard requirement by the base contract - to reflect the current balance of the underlying asset held by the vault.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import {ERC4626} from "@openzeppelin/contracts/token/ERC20/extensions/ERC4626.sol";
import {ERC20} from "@openzeppelin/contracts/token/ERC20/ERC20.sol";
import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";

contract VaultERC is ERC4626 {
    constructor(
        IERC20 asset_,
        string memory name_,
        string memory symbol_
    ) ERC20(name_, symbol_) ERC4626(asset_) {}

    function totalAssets() public view override returns (uint256) {
        return IERC20(asset()).balanceOf(address(this));
    }
}

The totalAssets() function simply returns the vault's balance of the underlying asset. While this implementation looks straightforward, its correctness is fundamental to the entire vault's accounting. If this function returns an incorrect value, all share calculations derived from it will be wrong.

The MockAssetA Contract

For verification purposes, we also need a mock ERC-20 token to serve as the underlying asset. The standard Solmate ERC20 implementation presents a challenge: it uses unchecked arithmetic in its transfer and transferFrom functions.

Under normal conditions, unchecked arithmetic is not an issue because the sum of all balances is not meant to exceed the ERC-20 totalSupply, which is guarded by safe math operations. However, when applying Certora formal verification, the prover introduces havocing - a process that randomly manipulates storage variables under specific conditions. This can cause token balances to assume values that lead to overflows, complicating the verification process.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import {ERC20} from "@openzeppelin/contracts/token/ERC20/ERC20.sol";

/// @notice Mock ERC20 with safe arithmetic for formal verification
contract MockAssetA is ERC20 {
    constructor() ERC20("MockAssetA", "MKA") {}

    function mint(address to, uint256 amount) external {
        _mint(to, amount);
    }
}

The MockAssetA contract overrides the transfer and transferFrom functions to remove unchecked arithmetic. While we could have constrained Certora's havocing through specification files by adding invariants as preconditions, a more straightforward solution is to modify the ERC-20 implementation itself to strictly adhere to safe arithmetic.

Setting Up the Verification Environment

The project is structured as a standard Foundry project, though the setup can be adapted to other frameworks. To run Certora formal verification, you need to install the Certora CLI and obtain an API key.

Installation

You can obtain a CERTORAKEY by registering at Certora's website. Store it as an environment variable so it persists across terminal sessions.

Project Structure

erc4626-certora/
  src/
    VaultERC.sol          # ERC-4626 vault contract
    MockAssetA.sol        # Safe-math ERC-20 mock
  certora/
    specs/
      ERC4626.spec        # Formal verification rules
    conf/
      ERC4626.conf        # Certora configuration
  foundry.toml
  package.json

Writing the Specification File

A spec file in Certora Prover is a formal verification script that defines the rules and constraints a smart contract must satisfy. Unlike traditional testing, which relies on specific inputs and outputs, a spec file enables mathematical reasoning over all possible states, ensuring the contract adheres to its intended logic under all conditions.

The Methods Block

The methods block defines which functions from the smart contracts will be used during the verification process. Function declarations match the actual functions in the VaultERC contract, and Certora verifies their behavior based on the rules defined in the spec.

methods {
    // VaultERC (ERC4626) functions
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function allowance(address, address) external returns (uint256) envfree;
    function totalAssets() external returns (uint256) envfree;

    // Underlying asset (MockAssetA) functions
    function asset.totalSupply() external returns (uint256) envfree;
    function asset.balanceOf(address) external returns (uint256) envfree;
    function asset.decimals() external returns (uint8) envfree;
}

Marking a method with envfree has two effects. First, calls to the method from CVL do not require an explicit environment value as the first argument. Second, the prover ensures that the method's implementation does not rely on any environment variable (such as msg.sender). During verification, the prover does not solely execute functions from VaultERC - we must also define additional functions in the methods block to inform the prover about other relevant methods it should consider.

Ghost Variables and Hooks

Ghost variables in Certora are state variables that exist only within the specification - they do not correspond to any storage in the actual contract. They are used to track derived properties that the prover needs to reason about.

For our ERC-4626 verification, we define ghost variables to track the sum of all balances across users:

// Ghost variable: tracks total sum of share balances
ghost mathint sumOfBalancesERC4626 {
    init_state axiom sumOfBalancesERC4626 == 0;
}

// Ghost variable: mirrors individual balances
ghost mapping(address => uint256) balanceOfMirroredERC4626;

// Ghost variable: tracks total sum of asset balances
ghost mathint sumOfBalancesERC20 {
    init_state axiom sumOfBalancesERC20 == 0;
}

// Ghost variable: mirrors individual asset balances
ghost mapping(address => uint256) balanceOfMirroredERC20;

Without an init_state axiom, the value of ghost variables would be havoced (randomized), leading to unpredictable verification outcomes. The axiom ensures that the sum starts at zero, matching the initial state of a freshly deployed contract.

Hooks intercept storage operations on the contract and update our ghost variables accordingly:

// Hook: update ghost variables when ERC4626 balances change
hook Sstore _balances[KEY address user] uint256 newBalance
    (uint256 oldBalance) {
    sumOfBalancesERC4626 = sumOfBalancesERC4626
        + newBalance - oldBalance;
    balanceOfMirroredERC4626[user] = newBalance;
}

// Hook: enforce balance constraint on load
hook Sload uint256 balance _balances[KEY address user] {
    require balanceOfMirroredERC4626[user] == balance;
}

The Sstore hook fires every time a balance is written to storage, updating our running sum. The Sload hook enforces consistency between the mirrored ghost variable and the actual storage value, ensuring the prover reasons correctly about individual balances.

Defining Invariants

Invariants are the core of formal verification. They are properties that must hold true after every state-changing operation on the contract. If an invariant is violated, it indicates an inconsistency in how tokens are being minted, burned, or transferred.

/// @title Total supply must equal sum of all individual balances
invariant sumOfBalancesEqualsTotalSupplyERC4626()
    to_mathint(totalSupply()) == sumOfBalancesERC4626;

/// @title Asset total supply must equal sum of all asset balances
invariant sumOfBalancesEqualsTotalSupplyERC20()
    to_mathint(asset.totalSupply()) == sumOfBalancesERC20;

/// @title Zero total assets implies zero share supply
invariant totalAssetsZeroImpliesTotalSupplyZero()
    totalAssets() == 0 => totalSupply() == 0;

/// @title Non-zero share supply requires non-zero asset supply
invariant totalSupplyMatch()
    totalSupply() > 0 => asset.totalSupply() > 0;

/// @title No single balance can exceed total supply (ERC4626)
invariant singleUserBalanceSmallerThanTotalSupplyERC4626(address user)
    balanceOf(user) <= totalSupply();

/// @title No single balance can exceed total supply (ERC20)
invariant singleUserBalanceSmallerThanTotalSupplyERC20(address user)
    asset.balanceOf(user) <= asset.totalSupply();

The sumOfBalancesEqualsTotalSupplyERC4626 invariant is particularly crucial. It ensures that the total supply of vault shares is always consistent with the sum of individual balances. A mismatch between totalSupply and sumOfBalances would indicate a bug in how tokens are being minted, burned, or transferred - requiring further investigation to identify the root cause.

Verification Rules

Beyond invariants, we define specific rules that verify the behavior of individual functions. Rules describe expected outcomes for operations like deposits and withdrawals:

/// @title Minting shares must increase total assets
rule mintMustIncreaseTotalAssets(env e, uint256 shares, address receiver) {
    uint256 totalAssetsBefore = totalAssets();

    mint(e, shares, receiver);

    uint256 totalAssetsAfter = totalAssets();

    assert totalAssetsAfter >= totalAssetsBefore,
        "Minting shares must not decrease total assets";
}

/// @title Monotonic relationship between supply and assets
rule assetAndShareMonotonicity(env e, method f, calldataarg args) {
    uint256 totalSupplyBefore = totalSupply();
    uint256 totalAssetsBefore = totalAssets();

    f(e, args);

    uint256 totalSupplyAfter = totalSupply();
    uint256 totalAssetsAfter = totalAssets();

    // If supply increased, assets must also increase (or stay same)
    assert totalSupplyAfter > totalSupplyBefore =>
        totalAssetsAfter >= totalAssetsBefore,
        "Supply increase without asset increase";

    // If supply decreased, assets must also decrease (or stay same)
    assert totalSupplyAfter < totalSupplyBefore =>
        totalAssetsAfter <= totalAssetsBefore,
        "Supply decrease without asset decrease";
}

The assetAndShareMonotonicity rule is particularly powerful because it uses method f with calldataarg args - meaning it applies to every function in the contract. The prover will test this monotonicity property across all possible function calls, not just deposit and withdraw.

Configuration File

The .conf file defines the inputs and settings for the verification process. It specifies which contracts to verify, which spec files to use, and other configuration options:

{
    "files": [
        "src/VaultERC.sol",
        "src/MockAssetA.sol"
    ],
    "verify": "VaultERC:certora/specs/ERC4626.spec",
    "link": [
        "VaultERC:_asset=MockAssetA"
    ],
    "solc": "solc0.8.20",
    "msg": "ERC4626 Vault Verification"
}

The link field is essential - it tells Certora that the _asset field in VaultERC should resolve to the MockAssetA contract. Without this linkage, the prover would not know how to reason about cross-contract interactions between the vault and its underlying asset.

Running the Verification

Once the spec file and configuration are ready, running the Certora Prover is straightforward:

The certoraRun utility handles the complete pipeline: it invokes the Solidity compiler, transforms the bytecode into an internal representation, and submits the verification job to Certora's cloud-based prover. Results become available on Certora's verification dashboard.

Understanding Verification Results

Once verification completes, Certora generates a detailed report containing:

• Successful checks: Properties that held true across all possible executions, shown with a green checkmark
• Failed checks: Violations of defined rules or invariants, with concrete counterexamples
• Vacuous rules: Rules that passed trivially because their preconditions were never satisfiable

The verification dashboard provides a structured breakdown of results. For each rule, you can inspect the call trace that the prover explored, including the specific function calls and state transitions that were analyzed.

Successful Verification Example

When a deposit operation is verified successfully, the report shows that both totalSupply and sumOfBalances increased by the same value, maintaining consistency. For example, a deposit function call with an amount of 0x1128 would show both values increasing by exactly that amount.

Detecting Bugs with Code Mutations

To validate that our specification is meaningful and can actually catch bugs, we can introduce intentional code mutations. For example, modifying the vault contract to mint extra shares or skip a balance update creates an imbalance between total supply and individual balances.

The prover correctly detects these mutations by reporting a violation of the sumOfBalancesEqualsTotalSupplyERC4626 invariant. The counterexample shows exactly which function call and state transition triggered the violation - confirming that the spec file can effectively catch such issues.

Handling Havocing and Overflow Challenges

One of the most common challenges when working with Certora Prover is dealing with havocing. The prover randomly manipulates storage variables to explore all possible states, which can cause token balances to assume values that lead to arithmetic overflows.

This issue is particularly relevant for ERC-20 tokens that use unchecked blocks for gas optimization. When the prover havoces a balance to type(uint256).max and then a transfer adds to it, an overflow occurs - not because of a real bug, but because the havoced state is unrealistic.

There are two main approaches to address this:

1. Constrain havocing via spec preconditions: Add invariants as preconditions to rules, limiting the states the prover explores to realistic ones
2. Modify the contract under test: Replace unchecked arithmetic with safe arithmetic in the test version (as we did with MockAssetA)

The second approach is often simpler and more reliable. By ensuring the ERC-20 mock uses checked arithmetic throughout, we eliminate overflow-related false positives without adding complexity to our specification.

Best Practices for Certora Verification

Based on our experience applying Certora Prover to production smart contracts at Zokyo, we recommend the following practices:

1. Start with fundamental invariants. Begin with properties like "totalSupply equals sum of balances" before writing complex rules. These catch the most critical bugs.
2. Use ghost variables and hooks strategically. They enable tracking aggregate properties (like total balance sums) that are impossible to express with contract storage alone.
3. Always initialize ghost variables. Without init_state axiom declarations, ghost variables are havoced, leading to spurious verification failures.
4. Link contracts explicitly. Cross-contract interactions must be declared in the .conf file. Missing links cause the prover to treat external calls as arbitrary (havoced) return values.
5. Validate specs with mutations. Introduce known bugs to confirm your specification actually detects them. A spec that never fails is likely vacuous.
6. Use envfree where appropriate. Marking view functions as envfree simplifies rule writing and makes the prover's reasoning more efficient.
7. Check for vacuity. A rule is vacuous if its precondition is never satisfiable. Certora flags these, but you should investigate any vacuous results to ensure your assumptions are correct.

Formal Verification vs. Traditional Testing

Formal verification complements traditional testing rather than replacing it. Here is how they compare:

• Unit tests: Verify specific scenarios with known inputs and expected outputs. Fast to write but limited by the developer's imagination.
• Fuzz testing: Generates random inputs to explore unexpected scenarios. Better coverage than unit tests but still probabilistic.
• Formal verification: Proves properties hold for all possible inputs and states. Provides mathematical guarantees but requires specification expertise.

The strongest security posture combines all three approaches. Unit tests catch regressions quickly, fuzz testing discovers edge cases, and formal verification provides definitive proof of correctness for critical properties.

Conclusion

Formal verification with Certora Prover is a powerful tool for ensuring the correctness of smart contract implementations. For ERC-4626 vaults, where precise accounting of assets and shares is critical, it provides mathematical guarantees that no amount of manual testing can match.

In this guide, we walked through the complete workflow: setting up the contract under test, writing specifications with ghost variables and hooks, defining invariants and rules, configuring the prover, and interpreting verification results. We also addressed practical challenges like havocing and overflow handling that arise during real-world verification.

Valid implementations pass verification, while intentional code mutations introducing inconsistencies are successfully detected by the specification. This demonstrates that formal verification is not just a theoretical exercise - it is a practical tool that catches real bugs.

At Zokyo, we integrate formal verification into our audit methodology for DeFi protocols, particularly those involving complex token accounting like ERC-4626 vaults. The mathematical rigor it provides is an essential layer of defense in an ecosystem where a single bug can mean irreversible financial loss.

If you are building a DeFi protocol and want help implementing formal verification or need a comprehensive security audit, reach out to our team.