Overview

Formal verification provides a rigorous method to mathematically prove that a smart contract adheres to its intended specifications, reducing the risk of vulnerabilities.

This article explores the process of formally verifying an ERC-4626 vault—a standardized tokenized yield-bearing vault—using Certora Prover. Certora Prover 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.

We plan to publish additional articles covering more aspects of formal verification in our DeFi example. By the end of this article, you will understand how to set up and run a minimal formal verification using Certora Prover to enhance the security and reliability of smart contracts.

Setup

To formally verify the ERC-4626 vault, we need to prepare the necessary Solidity smart contracts and Certora files. This example is structured as a Foundry project, though the setup can be adapted to other frameworks. The key components are:

• Smart Contracts

VaultERC.sol – The ERC-4626 vault implementation that is the subject of formal verification. This contract will be analyzed to ensure it adheres to the expected invariants.

MockAssetA.sol – A mock ERC-20 token that represents the underlying asset of the vault.

• Certora Files

VaultERC.spec – Defines the formal verification rules for VaultERC.sol. This file contains the key properties we aim to prove.

VaultERC.conf – Specifies how Certora should execute the verification, including contract inputs, constraints, and other various configuration settings.

To run the verification, Certora Prover must be installed. Follow the official installation guide here: 👉 Certora Installation Guide

With the setup complete, we can focus later on defining verification rules in VaultERC.spec. It is worth noting that we use the Solmate library: forge install transmissions11/solmate

Smart Contract Implementation

1. MockAssetA: A Tailored ERC20 Implementation

For our testing task, we require an ERC20 token to act as the underlying asset for our ERC4626 vault. While we could use the standard Solmate ERC20 implementation without changes, it presents a challenge due to the use of unchecked arithmetic in its transfer and transferFrom functions:

unchecked {

    balanceOf[to] += amount;

}

Under normal conditions, unchecked arithmetic is not an issue since the overflow is prevented by the fact that the sum of balances is not meant to exceed the ERC20 totalSupply which is guarded by safe maths 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.

While we could constrain Certora's havocing a variable in our specification files by adding an invariant and requiring it to be a precondition, a more straightforward solution right now is to modify the ERC20 implementation itself to strictly adhere to safe arithmetic. Since this token is merely a supporting asset in our tests, this modification does not impact our core ERC4626 contract behavior.

Implementation: MockAssetA

To address this, we introduce smart contract MockAssetA, an ERC20 token that overrides the transfer and transferFrom functions to remove unchecked arithmetic:

contract MockAssetA is ERC20 {

    constructor(string memory name_, string memory symbol_, uint8 decimals_) 

      ERC20(name_, symbol_, decimals_) {}

    function transfer(address to, uint256 amount) public override returns (bool) {

        balanceOf[msg.sender] -= amount;

        balanceOf[to] += amount;

        emit Transfer(msg.sender, to, amount);

        return true;

    }

    function transferFrom(address from, address to, uint256 amount) public override returns (bool) {

        uint256 allowed = my allowance[from][msg.sender];

        if (allowed != type(uint256).max) {

            allowance[from][msg.sender] = allowed - amount;

        }

        balanceOf[from] -= amount;

        balanceOf[to] += amount;

        emit Transfer(from, to, amount);

        return true;

    }

}

2. VaultERC: The ERC4626 Implementation Under Test

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

Implementation: VaultERC

pragma solidity >=0.8.0;

import {ERC20} from "solmate/tokens/ERC20.sol";

import {ERC4626} from "solmate/tokens/ERC4626.sol";

import {Owned} from "solmate/auth/Owned.sol";

contract VaultERC is Owned, ERC4626 {

    constructor(address _asset) 

        Owned(msg.sender)

        ERC4626(ERC20(_asset), "Vault Wrapper", "4626") 

    {}

    function totalAssets() public view override returns (uint256) {

        return asset.balanceOf(address(this));

    }

}

Formal Verification Specification: ERC4626.spec

A spec file in Certora Prover is a formal verification script that defines the rules and constraints a smart contract must satisfy. It serves as the blueprint for how the prover checks correctness by specifying invariants, function behaviors, and assumptions about the smart contract’s state.

Unlike traditional testing, which relies on specific inputs and outputs, a spec file enables mathematical reasoning over all possible states, ensuring that the smart contract adheres to its intended logic under all conditions, including edge cases.

We first start the ERC4626.spec specification file by the following statement:

ERC4626.spec

Using MockAssetA as AssetA;

This line establishes an alias for the MockAssetA contract, allowing us to refer to it as AssetA throughout the spec file.

At this point we fill the methods block in the file. The methods block in Certora's specification file defines which functions from our smart contracts will be used during the verification process.

methods{

    /// VaultERC methods

    function asset() external returns address envfree;

    function totalSupply() external returns uint256 envfree;

    function deposit(uint256,address) external;

    function mint(uint256,address) external;

    function withdraw(uint256,address,address) external;

    function redeem(uint256,address,address) external;

    function totalAssets() external returns uint256 envfree;

    ...

}

These function declarations match the actual functions in the VaultERC (ERC4626) contract. Certora will verify their behavior based on the rules we define in the spec. 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 in the verified contract does not rely on any that is considered an environment variable (e.g. 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.

function _.balanceOf(address) external  => DISPATCHER(true);

function _.transfer(address,uint256) external  => DISPATCHER(true);

function _.transferFrom(address,address,uint256) external => DISPATCHER(true);

function AssetA.balanceOf(address) external returns uint256 envfree;

function AssetA.allowance(address, address) external returns uint256 envfree;

function AssetA.transferFrom(address,address,uint256) external returns bool;

The first three entries do not specify a specific contract but instead use _ (a wildcard), meaning they apply to any contract that implements these methods. With DISPATCHER(true), these functions are treated as dispatcher summaries, allowing the Prover to dynamically resolve the actual implementation during the run. When executing these methods, the Prover will identify and apply the correct implementation from any contract included in the verification run, such as ERC20.sol, MockAssetA.sol, or others.

The last three entries explicitly reference AssetA, which is an alias for the MockAssetA contract. In this case, the Prover directly resolves these method implementations from MockAssetA.sol.

Ghost variables and hooks

At this stage, we define ghost variables, which serve as an 'extension' of the state of the contracts under verification.

ghost mathint sumOfBalances {

    init_state axiom sumOfBalances == 0;

}

init_state axiom sumOfBalances == 0; → Ensures that sumOfBalances is initialized to zero in the initial state. Without an init_state axiom, the value of sumOfBalances would be havoced (randomized).

The role of this ghost variable is to track the total sum of balances across all users throughout the run.

To make this ghost variable meaningful, we define hooks, which allow us to attach Certora Verification Language (CVL) code to specific low-level operations, such as reading from (Sload) or writing to (Sstore) storage variables.

Each hook consists of:

• A pattern that determines which operations will trigger the hook.

• A code block that executes when the specified operation occurs. Here's an example:

hook Sstore balanceOf[KEY address a] uint256 newValue (uint256 oldValue)  {

    sumOfBalances = sumOfBalances + newValue - oldValue;

}



This is triggered whenever the contract updates the storage of the balanceOf mapping for an arbitrary address a. The hook adjusts the total sum by adding the new balance and subtracting the old balance, ensuring that sumOfBalances correctly tracks all balance changes.

Another example:

hook Sload uint256 val balanceOf[KEY address a]  {

    require sumOfBalances >= val;

}

This is triggered whenever the contract reads a value from the balanceOf mapping in storage. It ensures that the total recorded sum of balances is always greater than or equal to the individual balance being read. This prevents inconsistencies, especially in cases where storage values could be havoced (randomized) during verification.

Invariants

The final step in the spec file is defining the invariant, which specifies a property that must always hold true throughout the execution of the contract.

Here is the invariant we define:

invariant totalSupplyIsSumOfBalances()

    totalSupply() == sumOfBalances;

This condition is straightforward—it asserts that the totalSupply() of the vault token must always be equal to sumOfBalances, which represents the sum of all balances in the balanceOf mapping.

Since we previously defined hooks to track updates to sumOfBalances, we know that it correctly reflects the cumulative balance of all token holders.

This invariant is crucial because it ensures that the total supply of tokens is always consistent with the sum of individual balances. If it is ever violated, it indicates an inconsistency in how tokens are being minted, burned, or transferred, requiring further investigation to identify a potential bug.

Running the spec file for verification

Writing the conf file

Once we have defined the ERC4626.spec file containing the formal verification rules, the next step is to run the Certora Prover to check whether our ERC4626 implementation adheres to that expected property. This requires configuring a .conf file to specify the contracts involved, the verification setup and other configuration settings.

• Setting Up the Configuration File

The following configuration file, ERC4626.conf, defines the inputs and settings for the verification process:

{

    "files": [

        "src/VaultERC.sol",

        "src/mocks/MockAssetA.sol"

    ],

    "verify": "VaultERC:certora/VaultERC.spec",

    "link": ["VaultERC:asset=MockAssetA"],

    "optimistic_loop": true,

    "rule_sanity": "basic",

    "msg": "ERC4626 certora formal verification"

}

With the configuration file in place, we can initiate the test by executing the following command:

certoraRun certora/ERC4626.conf

Once the verification process is completed, Certora will generate a detailed verification report containing:

✅ Successful Checks – Indicating which properties held true across all possible executions.
❌ Failed Checks – Showing violations of the defined rules or invariants.

Viewing the Results

To inspect the results, Certora provides an output link to its verification dashboard, where a structured breakdown of the results is available.

The following snapshot presents the test results of this run via the Certora Prover. Initially, the totalSupply variable in the VaultERC contract and the ghost variable sumOfBalances were both havoced and assigned a value of zero before execution.

The verification test executes a deposit function call with an amount of 0x1128. As expected, both totalSupply and sumOfBalances increase by this exact value, maintaining consistency between the two. This confirms that the total supply of vault tokens correctly reflects the sum of all balances, thereby satisfying the defined invariant.

It's important to note how the Certora Prover operates: it attempts to find counterexamples where our defined rules or invariants fail. If it cannot find a violation, it presents one valid example among an infinite number of possible executions where the invariant holds. The image shows such a successful case, reinforcing the correctness of our ERC4626 implementation for this particular scenario.

Testing the test!

Now, someone proposed a genius implementation (sarcasm intended) that gives away extra minted shares to the owner, modifying the afterDeposit function as follows:

function afterDeposit(uint256, uint256 shares) internal override {

    balanceOf[owner] += shares / 100;

}

This modification was added to VaultERC, where afterDeposit() is an ERC4626 hook that gets triggered after calling deposit and mint.

Running the Prover with This Change

After executing the verification process with this new implementation, the test results in the screenshot reveal a failure in both mint and deposit.

The invariant failed to invoke mint and deposit because the balanceOf mapping was modified to grant additional shares to the contract owner. However, totalSupply was not updated accordingly, causing an inconsistency. This led to a mismatch between totalSupply and sumOfBalances, breaking our invariant.

As a result, the prover correctly detected the issue, demonstrating that this code mutation violates the expected ERC4626 behavior by causing an imbalance between total supply and individual balances. The purpose of introducing this intentional bug was to verify that our spec file can effectively catch such violations. This approach helps ensure that our test is robust and capable of identifying real issues.

Conclusion

Formal verification using Certora Prover has proven to be a powerful tool for ensuring the correctness of our ERC4626 implementation. Through our test, we confirmed that valid implementations passed that verification, while intentional code mutations introducing inconsistencies were successfully detected. This demonstrates the effectiveness of our specification file in catching bugs and maintaining the integrity of the ERC4626 vault.

You can find an example in this GitHub repository.

By leveraging formal verification, we gain a higher level of confidence in the security and correctness of our contract, reducing potential vulnerabilities before deployment. This method complements traditional testing approaches by ensuring that the contract behaves correctly under all possible conditions, not just predefined test cases.