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.
Install Java
sudo apt update
sudo apt install default-jre
java -version
Install pipx
sudo apt install pipx
pipx ensurepath
Install Certora CLI
pipx install certora-cli
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
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.
Clone and build
git clone https://github.com/alexzoid-eth/2024-08-flayer-fv
cd 2024-08-flayer-fv/flayer
forge build
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.
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:
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:
Prerequirements (optional)
Constraints on the contract’s initial state or the environment before the rule runs, otherwise arbitrary state applied.
Contract Execution
One or more function calls.
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 {
_fee.validate();
PoolParams memory poolParams = _poolParams[_poolId];
poolParams.poolFee = _fee;
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
rule noOpFunctionDetection(env e, method f, calldataarg args)
filtered { f -> !f.isView && !f.isPure }
{
storage before = lastStorage;
f(e, args);
storage after = lastStorage;
satisfy(before[currentContract] != after[currentContract]);
}
How It Works
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.
Filters A filtered block lets us exclude specific methods like view and pure functions from testing. (Filters docs)
Storage Snapshots
We take a snapshot of the contract’s storage before the function call and another after it. (Storage docs)
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:
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:
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.
