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

## Intro

Curious about [Certora](https://x.com/CertoraInc) 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](https://solodit.cyfrin.io/issues/m-4-admin-can-not-set-the-pool-fee-since-it-is-only-set-in-memory-sherlock-flayer-git) discovered in the past [Sherlock](https://x.com/sherlockdefi) contest. Read on to learn more!

---

## Setup

Below is a quick guide on installing Certora and its dependencies on a fresh Ubuntu ([Installation docs](https://docs.certora.com/en/latest/docs/user-guide/install.html)). Skip this section if you already have Certora installed.

1. **Install** [**Java**](https://ubuntu.com/tutorials/install-jre#2-installing-openjdk-jre)
    
    ```bash
    sudo apt update
    sudo apt install default-jre
    java -version
    ```
    
2. **Install** [**pipx**](https://github.com/pypa/pipx)
    
    ```bash
    sudo apt install pipx
    pipx ensurepath
    ```
    
3. **Install Certora CLI**
    
    ```bash
    pipx install certora-cli
    ```
    
4. **Install** [**solc-select**](https://github.com/crytic/solc-select)
    
    ```bash
    pipx install solc-select
    ```
    
    Then install the Solidity compiler version that our project requires:
    
    ```bash
    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](https://discord.com/channels/795999272293236746/1080511450075893800) or on the [website](https://www.certora.com/signup). Once you have it, export it to your environment variables:
    
    ```bash
    echo "export CERTORAKEY=<your_certora_api_key>" >> ~/.bashrc
    ```
    

## Execute

Next, let’s clone [my repository](https://github.com/alexzoid-eth/2024-08-flayer-fv) (adapted from a Sherlock [contest](https://github.com/sherlock-audit/2024-08-flayer)) and run the Certora Prover.

1. **Clone and build**
    
    ```bash
    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:
    
    ```bash
    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](http://prover.certora.com).
    
3. **Certora Dashboard**  
    After running the command, you’ll see a unique URL such as:
    
    ```bash
    https://prover.certora.com/output/52567/ebcd153233744cc983869261222e416b/?anonymousKey=e4d88a2858d6cbf65b68ac391e25ce2a6f3a03b2
    ```
    
    Clicking this link or visiting the [dashboard](https://prover.certora.com/) 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](https://docs.certora.com/en/latest/docs/prover/cli/options.html)), using a `.conf` file often keeps things cleaner.

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

```json
{
    "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](https://docs.certora.com/en/latest/docs/prover/cli/conf-file-api.html)).

---

## 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:

```solidity
rule dummy() {
    assert(true);
}
```

* `assert(expr)`  
    Similar to Solidity’s `assert`, this requires that `expr` always holds on every valid execution path. ([assert docs](https://docs.certora.com/en/latest/docs/cvl/statements.html#assert-and-require))
    
* `satisfy(expr)`  
    A reachability requirement ensuring `expr` holds on at least one execution path. ([satisfy docs](https://docs.certora.com/en/latest/docs/cvl/statements.html#satisfy-statements))
    

### 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](https://solodit.cyfrin.io/issues/m-4-admin-can-not-set-the-pool-fee-since-it-is-only-set-in-memory-sherlock-flayer-git) 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](https://github.com/sherlock-audit/2024-08-flayer/blob/main/flayer/src/contracts/implementation/UniswapImplementation.sol#L783-L793)

```solidity
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](https://github.com/alexzoid-eth/2024-08-flayer-fv/blob/main/flayer/certora/specs/UniswapImplementation.spec)

```solidity
// 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](https://docs.certora.com/en/latest/docs/user-guide/parametric.html)) **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](https://docs.certora.com/en/latest/docs/cvl/rules.html#filters))
    
3. **Storage Snapshots**  
    We take a snapshot of the contract’s storage before the function call and another after it. ([Storage docs](https://docs.certora.com/en/latest/docs/cvl/expr.html#comparing-storage))
    
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

![](https://cdn.hashnode.com/res/hashnode/image/upload/v1739970916159/80ac66dc-48f8-4ffb-8774-048e09c17e79.png align="center")

After running the prover, I received this [link](https://prover.certora.com/output/52567/ebcd153233744cc983869261222e416b/?anonymousKey=e4d88a2858d6cbf65b68ac391e25ce2a6f3a03b2). The dashboard indicates several external functions in `UniswapImplementation.sol` are flagged by our rule:

* **Reverting by design**:  
    [afterInitialize()](https://github.com/Uniswap/v4-periphery/blob/870b46c06db6be34626d376800380638cbfe1133/src/base/hooks/BaseHook.sol#L63)  
    [beforeDonate()](https://github.com/Uniswap/v4-periphery/blob/870b46c06db6be34626d376800380638cbfe1133/src/base/hooks/BaseHook.sol#L124)  
    [afterDonate()](https://github.com/Uniswap/v4-periphery/blob/870b46c06db6be34626d376800380638cbfe1133/src/base/hooks/BaseHook.sol#L132)  
    [initializeCollection()](https://github.com/alexzoid-eth/2024-08-flayer-fv/blob/main/flayer/src/contracts/implementation/BaseImplementation.sol#L152)
    
* **Doing nothing but emitting an event**:  
    [afterAddLiquidity()](https://github.com/alexzoid-eth/2024-08-flayer-fv/blob/main/flayer/src/contracts/implementation/UniswapImplementation.sol#L647-L652)  
    [afterRemoveLiquidity()](https://github.com/alexzoid-eth/2024-08-flayer-fv/blob/main/flayer/src/contracts/implementation/UniswapImplementation.sol#L683-L688)
    

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()](https://github.com/alexzoid-eth/2024-08-flayer-fv/blob/main/flayer/src/contracts/implementation/UniswapImplementation.sol#L376-L420), which modifies another contract’s state,
    
* and [setFee()](https://github.com/alexzoid-eth/2024-08-flayer-fv/blob/main/flayer/src/contracts/implementation/UniswapImplementation.sol#L783-L793), where we found our real bug.
    

### After the Fix

![](https://cdn.hashnode.com/res/hashnode/image/upload/v1739970956384/22d9ee96-a0e4-4f13-a55b-c235c786a5b2.png align="center")

Once we fix the `setFee` function (using `storage` instead of `memory`) and rerun the verifier ([updated link](https://prover.certora.com/output/52567/36e0cd1ee2fa4253859f8f138758ac60/?anonymousKey=bde4d53fcac88585047f9e47e57a0446d73cf8a4)), 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.