First steps with Certora Formal Verification: Catching a Real Bug with a Universal 5-Line Rule

Intro

Curious about Certora Formal Verification but unsure where to begin? This tutorial provides a step-by-step setup and a powerful five-line rule for catching a very common class of storage-related bugs. It’s illustrated with a real issue discovered in the past Sherlock contest. Read on to learn more!

---

Setup

Below is a quick guide on installing Certora and its dependencies on a fresh Ubuntu (Installation docs). Skip this section if you already have Certora installed.

1. Install Java

    sudo apt update
    sudo apt install default-jre
    java -version
   

2. Install pipx

    sudo apt install pipx
    pipx ensurepath
   

3. Install Certora CLI

    pipx install certora-cli
   

4. Install solc-select

    pipx install solc-select
   

   Then install the Solidity compiler version that our project requires:

    solc-select install 0.8.24
    solc-select use 0.8.24
   

5. Set up Certora key
   You can get a free Certora key through their discord or on the website. Once you have it, export it to your environment variables:

    echo "export CERTORAKEY=<your_certora_api_key>" >> ~/.bashrc
   

Execute

Next, let’s clone my repository (adapted from a Sherlock contest) and run the Certora Prover.

1. Clone and build

    git clone https://github.com/alexzoid-eth/2024-08-flayer-fv
    cd 2024-08-flayer-fv/flayer
    forge build
   

2. Run Certora
   The Certora CLI command certoraRun accepts a JSON configuration file path:

    certoraRun certora/confs/UniswapImplementation.conf
   

   This compiles your Solidity files and uploads them, along with the specification and .conf file, to Certora’s remote prover. A link to the live job will appear in your terminal, and you can also monitor the process at prover.certora.com.

3. Certora Dashboard
   After running the command, you’ll see a unique URL such as:

    https://prover.certora.com/output/52567/ebcd153233744cc983869261222e416b/?anonymousKey=e4d88a2858d6cbf65b68ac391e25ce2a6f3a03b2
   

   Clicking this link or visiting the dashboard shows your job’s verification progress and results. Note: Because the URL contains an anonymousKey, anyone with that link can view your Solidity code and spec. If you prefer to share it privately (e.g., with Certora support), omit the /?anonymousKey=... part.

---

Configuration

A Certora configuration file is a convenient way to instruct the prover on how to handle your specifications and Solidity sources. Although you can provide these options via command line arguments (CLI docs), using a .conf file often keeps things cleaner.

https://github.com/alexzoid-eth/2024-08-flayer-fv/blob/main/flayer/certora/confs/UniswapImplementation.conf

{
    "files": [ 
        "src/contracts/implementation/UniswapImplementation.sol",
    ],
    "verify": "UniswapImplementation:certora/specs/UniswapImplementation.spec",
}

In our case, the minimal configuration contains two json key fields:

• files: An array of Solidity source files to compile and analyze.

• verify: The ContractName:PathToSpecFile indicating which contract to verify and which spec file to apply.

You can also include more advanced settings (Config docs).

---

Specification

A Certora specification is stored in a file ending with .spec and is written in the Certora Verification Language (CVL), which resembles Solidity. Each rule in your spec must include at least one assert() or satisfy() statement:

rule dummy() {
    assert(true);
}

• assert(expr)
  Similar to Solidity’s assert, this requires that expr always holds on every valid execution path. (assert docs)

• satisfy(expr)
  A reachability requirement ensuring expr holds on at least one execution path. (satisfy docs)

Typical Rule Structure

A CVL rule can be divided into three logical sections:

1. Prerequirements (optional)
   Constraints on the contract’s initial state or the environment before the rule runs, otherwise arbitrary state applied.

2. Contract Execution
   One or more function calls.

3. Statements
   The final assert/satisfy statements that verify or require certain conditions to hold after execution.

---

Real-Life Example

Here’s a practical demonstration of a rule for catching a real bug I found in a past Sherlock contest. The contract’s admin function stored an updated parameter in memory instead of storage, so changes were never persisted.

https://github.com/sherlock-audit/2024-08-flayer/blob/main/flayer/src/contracts/implementation/UniswapImplementation.sol#L783-L793

function setFee(PoolId _poolId, uint24 _fee) public onlyOwner {
    // Validate the fee amount
    _fee.validate();

    // Set our pool fee overwrite value
    PoolParams memory poolParams = _poolParams[_poolId]; // <-- "memory" instead of "storage"
    poolParams.poolFee = _fee;

    // Emit our event
    emit PoolFeeSet(poolParams.collection, _fee);
}

To detect this and similar issues automatically, we can craft a universal rule in plain English:

“Every non-view function must change contract storage in at least one execution path.”

Below is our Certora rule that implements this idea:

https://github.com/alexzoid-eth/2024-08-flayer-fv/blob/main/flayer/certora/specs/UniswapImplementation.spec

// Ensures that any non-view function changes storage
rule noOpFunctionDetection(env e, method f, calldataarg args)
    filtered { f -> !f.isView && !f.isPure }
{
    // 1. Prerequirements: Save contract storage before the call
    storage before = lastStorage;

    // 2. Contract Execution: Call the function with arbitrary arguments
    f(e, args);

    // 3. Statements: Storage not equal on at least one execution path
    storage after = lastStorage;
    satisfy(before[currentContract] != after[currentContract]);
}

How It Works

1. Parametric Rule
   The env e, method f, calldataarg args parameters with f(e, args) call instruct the Certora Prover to execute each relevant function with all possible inputs and environment variables (like msg.sender, timestamp, etc.). (Parametric docs) Note: It doesn’t matter whether you declare these variables inside the rule body or pass them as function arguments.

2. Filters A filtered block lets us exclude specific methods like view and pure functions from testing. (Filters docs)

3. Storage Snapshots
   We take a snapshot of the contract’s storage before the function call and another after it. (Storage docs)

4. satisfy() Statement
   By requiring before[currentContract] != after[currentContract], we ensure that at least one execution path of any non-view function must modify contract storage. If a function never modifies storage in any path, the rule fails, flagging a potential no-op bug.

This rule is broadly reusable - just drop it into other auditing projects to reveal any non-view functions that fail to persist changes.

---

Dashboard Analysis

After running the prover, I received this link. The dashboard indicates several external functions in UniswapImplementation.sol are flagged by our rule:

• Reverting by design:
  afterInitialize()
  beforeDonate()
  afterDonate()
  initializeCollection()

• Doing nothing but emitting an event:
  afterAddLiquidity()
  afterRemoveLiquidity()

These scenarios produce false positives for our no-op rule, as the functions either revert immediately or only emit an event.

The remaining flagged functions include:

• unlockCallback(), which modifies another contract’s state,

• and setFee(), where we found our real bug.

After the Fix

Once we fix the setFee function (using storage instead of memory) and rerun the verifier (updated link), our noOpFunctionDetection rule no longer flags setFee, confirming that the bug is resolved.

This demonstrates how a small, generic specification can quickly catch common issues.