# Find Highs Before External Auditors Using Certora Formal Verification

At [DeFi Security Summit 2024](https://defisecuritysummit.org/conference-2024/) I presented a workshop on how smart contract developers can use [invariant fuzz testing to find high severity issues](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing) prior to external audit, based on my real-world experience doing private audits with Cyfrin.

Since fuzz testing may seem daunting at first, I presented a simple methodology for learning to [“Think In Invariants”](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-thinking-in-invariants) that any developer could learn and apply to start building effective invariant fuzz testing suites. In response many researchers and developers reached out asking if a similar approach could be used with Formal Verification (FV) and the answer is a resounding “Yes”, though with some modifications.

This article will showcase using [Certora Verification Language](https://docs.certora.com/en/latest/docs/cvl/index.html) (CVL) to solve the same simplified versions of real world vulnerabilities from my previous invariant fuzz testing deep dive. Certora graciously provides a generous free tier which anyone can sign up for that I continuously used to create these solutions (including *many* failed attempts) and still didn’t get close to reaching the limit, so [sign up today](https://www.certora.com/signup?plan=prover&utm=updraft)!

Special thanks also to:

* [Updraft Assembly & Formal Verification Course](https://updraft.cyfrin.io/courses/formal-verification) which is free and great for learning Certora!
    
* [alexzoid\_eth](https://x.com/alexzoid_eth) who provided invaluable assistance improving some of the solutions
    
* [kirsteinuri](https://x.com/kirsteinuri) for reviewing this article and providing valuable corrections
    

Before we get to the Certora solutions lets briefly examine some important differences between how to use invariant fuzzers and Certora.

## Invariant Fuzz Testing vs Formal Verification

Everything regarding “thinking in invariants” still applies and carries over from fuzz testing into formal verification - we need to specify [useful properties](https://github.com/Certora/Tutorials/blob/master/06.Lesson_ThinkingProperties/Categorizing_Properties.pdf) to make effective use of both fuzz testing and formal verification. However some notable differences include:

### Solidity vs Certora Verification Language (CVL)

Our fuzzers were all written in Solidity but when using Certora we write “specifications” using Certora’s domain-specific language, CVL. These specifications are used as input to Certora’s “Prover” which compares rules in the specification against the underlying smart contract being verified to identify scenarios which could lead to assertions being violated. Writing specifications in CVL takes some getting used to but is very powerful, allowing the creation of elegant and concise solutions compared to much bulkier fuzzers, as we’ll soon see.

### Fuzz Locally vs Cloud Formal Verification

The fuzzers we wrote all ran locally, though since we used the Chimera framework they could easily be run in the cloud using [getrecon.xyz](https://getrecon.xyz/). In contrast Certora’s command-line tool will do some basic error checking and compilation then send it to the cloud for execution; the results can take anywhere from 30-60 seconds to be visible in Certora’s web interface.

### Fuzz Setup vs Formal Verification Relationships

A fuzz test over one or more smart contracts will typically:

* create contracts through their constructors, setting important parameters to specific values
    
* call any initialization functions, setup roles and grant permissions
    
* wrap the contract’s underlying functions using [“handler”](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-handlers-vs-no-handlers) functions which update ghost variables and satisfy preconditions reducing the amount of wasted fuzz runs
    

Within the environment we’ve created the fuzzer tries many random combinations of function calls attempting to break the defined invariants. One important consequence of this approach is that all of the restrictions on parameter values in `require` statements within the contract being fuzzed are respected, such that if the fuzzer breaks an invariant there is a high likelihood that will be a valid finding.

In contrast when using Certora there is no “setup” function, we aren’t explicitly creating the contracts, setting parameters or writing any Solidity. Instead we:

* define a `.conf` [configuration](https://docs.certora.com/en/latest/docs/prover/cli/conf-file-api.html) file with some basic information - the contracts we are testing and optional Certora flags
    
* write a `.spec` [specification](https://docs.certora.com/en/latest/docs/cvl/overview.html) file containing our Certora specification using CVL which defines invariants and relationships between objects (such as storage locations or environment parameters) using CVL `require` statements to restrict Certora from breaking invariants by reaching an invalid state
    

One benefit is that Certora specifications can be very concise compared to much bulkier fuzz testing code. However one drawback is that some restrictions present in the underlying contracts may need to be duplicated in the specification using CVL `require` statements to prevent Certora from setting storage slots to values that would never be possible and hence breaking invariants through invalid states.

### Fuzz Invariant vs Certora `rule` and `invariant`

All 3 fuzzers we used generally have the same type of invariant; a function that either returns a boolean (Echidna/Medusa) or fails an assert (Foundry). In contrast Certora has two ways to implement an “invariant”, using the `rule` and `invariant` keywords.

* [`rule`](https://docs.certora.com/en/latest/docs/cvl/rules.html) is ideally used when describing a conditional “scenario” to Certora; the conditions are expressed using a set of `require` statements that specify relationships between storage and/or environment. The conditions are followed by one or more `assert` or [`satisfy`](https://docs.certora.com/en/latest/docs/cvl/statements.html#satisfy) statements which are the actual properties we are trying to break
    
* [`invariant`](https://docs.certora.com/en/latest/docs/cvl/invariants.html) doesn’t support scenarios and is best used for simple boolean expressions which should always be true
    

Personally I found `rule` to be the most powerful so that is what most of our solutions use.

### Fuzz Cheat Codes vs Certora `env`

In our fuzz handlers we used a number of cheat codes such as `vm.prank` to change `msg.sender` or `vm.warp` to set `block.timestamp`. In contrast Certora has a special [`env`](https://docs.certora.com/en/latest/docs/cvl/types.html#env) type which is:

* declared and passed as the first parameter to underlying function calls
    
* used together with CVL `require` statements to constrain environment properties such as `msg.sender` or `block.timestamp`
    

### Additional Certora Features

Certora has a number of very powerful additional features including [parametric rules](https://docs.certora.com/en/latest/docs/user-guide/parametric.html) and [opcode hooks](https://docs.certora.com/en/latest/docs/user-guide/opcodes.html) - keep the [user guide](https://docs.certora.com/en/latest/docs/user-guide/index.html) open as a handy reference. There are also a number of important command-line parameters which we encode in the `.conf` files, the most important being [`optimistic_loop`](https://docs.certora.com/en/latest/docs/prover/cli/options.html#optimistic-loop) and [`optimistic_fallback`](https://docs.certora.com/en/latest/docs/prover/cli/options.html#optimistic-fallback).

Now that we are aware of important differences between using fuzz testing and Certora, let’s see what the Certora specifications look like for each of the simplified real-world vulnerabilities we solved in the invariant fuzzing deep dive!

## Example 1 - Flash Loan Denial Of Service

Specification: there are 2 contracts [`Receiver`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/02-unstoppable/ReceiverUnstoppable.sol) and [`Lender`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/02-unstoppable/UnstoppableLender.sol). `Receiver` has a function `executeFlashLoan` that calls `Lender::flashLoan` to take a flash loan, and the important invariant is that `Receiver` should always be able to take a flash loan if `Lender` has sufficient tokens available. First we create the configuration file [`certora.conf`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/02-unstoppable/certora.conf):

```json
{
  "files": [
    "src/02-unstoppable/ReceiverUnstoppable.sol",
    "src/02-unstoppable/UnstoppableLender.sol",
    "src/TestToken.sol"
  ],
  "verify": "ReceiverUnstoppable:test/02-unstoppable/certora.spec",
  "link": [
        "ReceiverUnstoppable:pool=UnstoppableLender",
        "UnstoppableLender:damnValuableToken=TestToken"
    ],
  "packages":[
        "@openzeppelin=lib/openzeppelin-contracts"
    ],
  "optimistic_loop": true
}
```

The Certora configuration:

* defines the Solidity source `files` required for the test
    
* marks the contract to `verify` and the `certora.spec` file which contains the Certora specification that will be sent to the Prover
    
* for contracts which have references to other contracts, instructs Certora to `link` those storage variables to the appropriate contract type
    
* necessary `packages` for library paths similar to Foundry remappings
    
* add an optional command-line parameter `optimistic_loop` required to prevent unnecessary counterexamples from incomplete loop iterations due to the Prover's bounded model checking
    

Then put our Certora specification in [`certora.spec`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/02-unstoppable/certora.spec):

```solidity
using ReceiverUnstoppable as receiver;
using UnstoppableLender as lender;
using TestToken as token;

methods {
    // `dispatcher` summary to prevent HAVOC
    function _.receiveTokens(address tokenAddress, uint256 amount) external => DISPATCHER(true);

    // `envfree` definitions to call functions without explicit `env`
    function token.balanceOf(address) external returns (uint256) envfree;
}

// executeFlashLoan() -> f() -> executeFlashLoan() should always succeed
rule executeFlashLoan_mustNotRevert(uint256 loanAmount) {
    // enforce valid msg.sender:
    // 1) not a protocol contract
    // 2) equal to ReceiverUnstoppable::owner
    env e1;
    require e1.msg.sender != currentContract &&
            e1.msg.sender != lender &&
            e1.msg.sender != receiver &&
            e1.msg.sender != token &&
            e1.msg.sender == receiver.owner &&
            e1.msg.value  == 0; // not payable

    // enforce sufficient tokens exist to take out flash loan
    require loanAmount > 0 && loanAmount <= token.balanceOf(lender);

    // first executeFlashLoan() succeeds
    executeFlashLoan(e1, loanAmount);

    // perform another arbitrary successful transaction f()
    env e2;
    require e2.msg.sender != currentContract &&
            e2.msg.sender != lender &&
            e2.msg.sender != receiver &&
            e2.msg.sender != token;
    method f;
    calldataarg args;
    f(e2, args);

    // second executeFlashLoan() should always succeed; there should
    // exist no previous transaction f() that could make it fail
    executeFlashLoan@withrevert(e1, loanAmount);
    assert !lastReverted;
}
```

The Certora specification contains:

* a `methods` section giving Certora some additional information about functions in the underlying contracts, the most common of these being marking `view` functions as `envfree` so that Certora’s special `env` type does not need to be passed as an input parameter when calling them
    
* a `rule` describing the “scenario” we wish to test
    
* `require` statements which restrict the `env` environment especially `msg.sender` and also instruct Certora to satisfy preconditions such as sufficient tokens being available for the flash loan
    
* a first `executeFlashLoan` call which always succeeds
    
* a [parametric](https://docs.certora.com/en/latest/docs/user-guide/parametric.html) function call instructing Certora to perform any arbitrary successful function call `f()`
    
* a second `executeFlashLoan` call using `@withrevert` to consider scenarios where this call may revert
    
* an assertion which fails if the previous call reverts, meaning Certora has broken the `rule` and hence found a valid attack path
    

## Example 2 - Reward Distribution Stuck

Specification: a [`Proposal`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/03-proposal/Proposal.sol) contract is deployed by a DAO with some ETH to be distributed if the proposal succeeds:

* `Proposal` is active until voting has finished or the proposal has timed out
    
* While active, eligible voters can vote `for` or `against`
    
* if quorum is reached the ETH should be distributed between the `for` voters
    
* otherwise the ETH should be refunded to the proposal creator
    

Our Certora specification uses an `invariant` construction which is very similar to the [fuzzer invariant](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-example-2-reward-distribution-stuck) we used for this challenge, but note the total absence of any setup, handlers or other “infrastructure” - everything is self-contained within the [`certora.spec`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/03-proposal/certora.spec) file:

```solidity
methods {
    // `envfree` definitions to call functions without explicit `env`
    function isActive() external returns (bool) envfree;
}

// define constants and require them later to prevent HAVOC into invalid state
definition MIN_FUNDING() returns uint256 = 1000000000000000000;
definition MIN_VOTERS()  returns uint256 = 3;
definition MAX_VOTERS()  returns uint256 = 9;

// Proposal state must be:
// 1) active with balance >= min_funding OR
// 2) not active with balance == 0
invariant proposal_complete_all_rewards_distributed()
    (isActive()  && nativeBalances[currentContract] >= MIN_FUNDING()) ||
    (!isActive() && nativeBalances[currentContract] == 0)
{
    // enforce state requirements to prevent HAVOC into invalid state
    preserved {
        // enforce valid total allowed voters
        require(currentContract.s_totalAllowedVoters >= MIN_VOTERS() &&
                currentContract.s_totalAllowedVoters <= MAX_VOTERS() &&
                // must be odd number
                currentContract.s_totalAllowedVoters % 2 == 1);

        // enforce valid for/against votes matches total current votes
        require(currentContract.s_votersFor.length +
                currentContract.s_votersAgainst.length
                == currentContract.s_totalCurrentVotes);

        // enforce that when a proposal is active, the total number of current
        // votes must be at maximum half the total allowed voters, since proposal
        // is automatically finalized once >= 51% votes are cast
        require(!isActive() || 
                    (isActive() && 
                    currentContract.s_totalCurrentVotes <= currentContract.s_totalAllowedVoters/2)
                );
    }
}
```

Since there is no setup we used `require` statements within a `preserved` block inside the `invariant` to enforce valid values for key contract parameters. Normally the smart contract’s constructor would enforce these restrictions but Certora sets storage slots to arbitrary values after the constructor. Using `require` statements we define relationships which restrict the range of possible values, preventing Certora from breaking the invariant due to an invalid state.

Also of note is the usage of `currentContract` - a special keyword that allows direct access to the underlying contract being verified.

## Example 3 - Voting Power Destruction

Specification: a [`VotingNft`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/04-voting-nft/VotingNftForFuzz.sol) contract:

* allows users to deposit ETH collateral against their NFT to give it DAO voting power
    
* NFTs can be created by the owner until the “power calculation start time”
    
* Once power calculation begins all NFTs start with max voting power which declines over time for NFTs which have not been backed by deposited ETH
    
* NFT voting power which has declined can never be increased; depositing the required ETH collateral simply prevents any future decrease
    

Using a `rule` construction we approximate the same invariant as the [fuzz test](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-example-3-voting-power-destruction) in our [Certora specification](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/03-proposal/certora.spec):

```solidity
methods {
    // `envfree` definitions to call functions without explicit `env`
    function getTotalPower()    external returns (uint256) envfree;
    function totalSupply()      external returns (uint256) envfree;
    function owner()            external returns (address) envfree;
    function ownerOf(uint256)   external returns (address) envfree;
    function balanceOf(address) external returns (uint256) envfree;
}

// define constants and require them later to prevent HAVOC into invalid state
definition PERCENTAGE_100() returns uint256 = 1000000000000000000000000000;

// given: safeMint() -> power calculation start time -> f()
// there should exist no f() where a permissionless attacker
// could nuke total power to 0 when power calculation starts
rule total_power_gt_zero_power_calc_start(address to, uint256 tokenId) {
    // enforce basic sanity checks on variables set during constructor
    require currentContract.s_requiredCollateral > 0 &&
            currentContract.s_powerCalcTimestamp > 0 &&
            currentContract.s_maxNftPower > 0 &&
            currentContract.s_nftPowerReductionPercent > 0 &&
            currentContract.s_nftPowerReductionPercent < PERCENTAGE_100();

    // enforce no nfts have yet been created; in practice some may
    // exist in storage though due to certora havoc
    require totalSupply() == 0 && getTotalPower() == 0 && balanceOf(to) == 0;

    // enforce msg.sender as owner required to mint nfts
    env e1;
    require e1.msg.sender == currentContract.owner();

    // enforce block.timestamp < power calculation start time
    // so new nfts can still be minted
    require e1.block.timestamp < currentContract.s_powerCalcTimestamp;

    // first safeMint() succeeds
    safeMint(e1, to, tokenId);

    // sanity check results of first mint
    assert totalSupply() == 1 && balanceOf(to) == 1 && ownerOf(tokenId) == to &&
           getTotalPower() == currentContract.s_maxNftPower;

    // perform any arbitrary successful transaction at power calculation
    // start time, where msg.sender is not an nft owner or an admin
    env e2;
    require e2.msg.sender != currentContract &&
            e2.msg.sender != to &&
            e2.msg.sender != currentContract.owner() &&
            balanceOf(e2.msg.sender) == 0 &&
            e2.block.timestamp == currentContract.s_powerCalcTimestamp;
    method f;
    calldataarg args;
    f(e2, args);

    // total power should not equal to 0
    assert getTotalPower() != 0;
}
```

Note again the usage of `require` statements to prevent corruption of the initial storage state which would lead to the invariant being broken due to an invalid state.

## Example 4 - Token Sale Drain

Specification: a [`TokenSale`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/05-token-sale/TokenSale.sol) contract:

* allows a DAO to sell its governance `sellToken` for another `buyToken`
    
* the token sale is only for allowed users and each user can only buy up to a max per-user limit to prevent concentration of voting power
    
* in our simplified version we assume an exchange rate of 1:1 and that `sellToken` always has decimals greater or equal to `buyToken`
    

This underlying contract uses two tokens; we found that in the configuration it was necessary to specify a different contract for each token otherwise the formal verification would “pass” but without actually running due to [vacuity](https://docs.certora.com/projects/tutorials/en/latest/lesson2_started/vacuity.html). The [`certora.conf`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/05-token-sale/certora.conf) looks like this:

```solidity
{
  "files": [
    "src/05-token-sale/TokenSale.sol",
    "src/TestToken.sol",
    "src/TestToken2.sol"
  ],
  "verify": "TokenSale:test/05-token-sale/certora.spec",
  "link": [
        "TokenSale:s_sellToken=TestToken",
        "TokenSale:s_buyToken=TestToken2"
  ],
  "packages":[
        "@openzeppelin=lib/openzeppelin-contracts"
  ],
  "optimistic_fallback": true,
  "optimistic_loop": true
}
```

For the Certora [specification](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/05-token-sale/certora.spec) we implemented the two [fuzzer invariants](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-example-4-token-sale-drain) using one `rule` per invariant which worked very well:

```solidity
methods {
    // `envfree` definitions to call functions without explicit `env`
    function getSellTokenSoldAmount() external returns (uint256) envfree;
}

// define constants and require them later to prevent HAVOC into invalid state
definition MIN_PRECISION_BUY() returns uint256 = 6;
definition PRECISION_SELL()    returns uint256 = 18;
definition FUNDING_MIN()       returns uint256 = 100;
definition BUYERS_MIN()        returns uint256 = 3;

// the amount of tokens bought should equal the amount of tokens sold
// due to 1:1 exchange ratio
rule tokens_bought_eq_tokens_sold(uint256 amountToBuy) {
    env e1;

    uint8 sellTokenDecimals = currentContract.s_sellToken.decimals(e1);
    uint8 buyTokenDecimals  = currentContract.s_buyToken.decimals(e1);

    // enforce basic sanity checks on variables set during constructor
    require currentContract.s_sellToken != currentContract.s_buyToken &&
            sellTokenDecimals == PRECISION_SELL()    &&
            buyTokenDecimals  >= MIN_PRECISION_BUY() &&
            buyTokenDecimals  <= PRECISION_SELL()    &&
            currentContract.s_sellTokenTotalAmount >= FUNDING_MIN() * 10 ^ sellTokenDecimals &&
            currentContract.s_maxTokensPerBuyer <= currentContract.s_sellTokenTotalAmount &&
            currentContract.s_totalBuyers >= BUYERS_MIN();

    // enforce valid msg.sender
    require e1.msg.sender != currentContract.s_creator &&
            e1.msg.sender != currentContract.s_buyToken &&
            e1.msg.sender != currentContract.s_sellToken &&
            e1.msg.value == 0;

    // enforce buyer has not yet bought any tokens being sold
    require currentContract.s_sellToken.balanceOf(e1, e1.msg.sender) == 0 &&
            getSellTokenSoldAmount() == 0;

    // enforce buyer has tokens with which to buy tokens being sold
    uint256 buyerBuyTokenBalPre = currentContract.s_buyToken.balanceOf(e1, e1.msg.sender);
    require buyerBuyTokenBalPre > 0 && amountToBuy > 0;

    // perform a successful `buy` transaction
    buy(e1, amountToBuy);
    
    // buyer must have received some tokens from the sale
    assert getSellTokenSoldAmount() > 0;
    uint256 buyerSellTokensBalPost = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);
    assert buyerSellTokensBalPost > 0;

    uint256 buyerBuyTokenBalPost = currentContract.s_buyToken.balanceOf(e1, e1.msg.sender);

    // verify buyer paid 1:1 for the tokens they bought when accounting for decimal difference
    assert getSellTokenSoldAmount() == (buyerBuyTokenBalPre - buyerBuyTokenBalPost) 
                                       * 10 ^ (sellTokenDecimals - buyTokenDecimals);
}

// this rule was provided by https://x.com/alexzoid_eth
rule max_token_buy_per_user(env e1, env e2, uint256 amountToBuy1, uint256 amountToBuy2) {   
    // enforce valid initial state
    require(currentContract.s_maxTokensPerBuyer <= currentContract.s_sellTokenTotalAmount);

    // enforce same buyer in different calls
    require e1.msg.sender == e2.msg.sender;
    require e1.msg.sender != currentContract && e1.msg.sender != currentContract.s_creator;

    // save initial balance
    mathint balanceBefore = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);
    
    // prevent over-flow in ERC20 (otherwise totalSupply and balances synchronization required)
    require balanceBefore < max_uint128 && amountToBuy1 < max_uint128 && amountToBuy2 < max_uint128;

    // perform two separate buy transactions
    buy(e1, amountToBuy1);
    buy(e2, amountToBuy2);

    // save final balance
    mathint balanceAfter = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);

    // verify total bought by same user must not exceed max limit per user
    mathint totalBuy = balanceAfter > balanceBefore ? balanceAfter - balanceBefore : 0;
    assert totalBuy <= currentContract.s_maxTokensPerBuyer;
}
```

## Example 5 - Vesting Points Increase

Specification: a [`Vesting`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/09-vesting/Vesting.sol) contract allocates points to users which can be used to redeem tokens once their vesting period has been served. The contract implements an [initialization invariant](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/09-vesting/Vesting.sol#L37) in the `constructor` ensuring that all points are allocated:

```solidity
require(totalPoints == TOTAL_POINTS, "Not enough points");
```

Users can transfer their points to another address but apart from this users have no way to increase or decrease their allocated points, hence the sum of individual user points should always remain equal to the initial total allocated.

Instead of re-implementing the same invariant as the fuzzer, I used Certora’s parametric rules to implement a much simpler [`rule`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/09-vesting/certora.spec#L4-L23) that achieves the same outcome:

```solidity
// there should exist no function f() that allows a user
// to increase their allocated points
rule user_cant_increase_points(address user) {
    require user != currentContract;

    // enforce that user has some allocated points
    uint24 userPointsPre = currentContract.allocations[user].points;
    require userPointsPre > 0;

    // user performs any arbitrary successful transaction f()
    env e;
    require e.msg.sender == user;
    method f;
    calldataarg args;
    f(e, args);

    // verify that no transaction exists which allows user to
    // increase their allocated points
    assert userPointsPre >= currentContract.allocations[user].points;
}
```

This elegant and concise solution beautifully illustrates the powerful nature of Certora’s Verification Language especially when using parametric rules. [alexzoid\_eth](https://x.com/alexzoid_eth) also implemented another [`rule`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/09-vesting/certora.spec#L26-L98) which uses the same idea as the [fuzzer invariant](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-example-5-vesting-points-increase):

```solidity
// sum of users' individual points should always remain equal to TOTAL_POINTS
// solution provided by https://x.com/alexzoid_eth
methods {
    function TOTAL_POINTS_PCT() external returns uint24 envfree => ALWAYS(100000);
}

// tracks the address of user whose points have increased
ghost address targetUser;

// ghost mapping to track points for each user address
ghost mapping (address => mathint) ghostPoints {
    axiom forall address user. ghostPoints[user] >= 0 && ghostPoints[user] <= max_uint24;
}

// hook to verify storage reads match ghost state
hook Sload uint24 val allocations[KEY address user].points {
    require(require_uint24(ghostPoints[user]) == val);
} 

// hook to update ghost state on storage writes
// also tracks first user to receive a points increase
hook Sstore allocations[KEY address user].points uint24 val {
    // Update targetUser only if not set and points are increasing
    targetUser = (targetUser == 0 && val > ghostPoints[user]) ? user : targetUser;
    ghostPoints[user] = val;
}

function initialize_constructor(address user1, address user2, address user3) {
    // Only user1, user2, and user3 can have non-zero points
    require(forall address user. user != user1 && user != user2 && user != user3 => ghostPoints[user] == 0);
    // Sum of their points must equal total allocation (100%)
    require(ghostPoints[user1] + ghostPoints[user2] + ghostPoints[user3] == TOTAL_POINTS_PCT());
}

function initialize_env(env e) {
    // Ensure message sender is a valid address
    require(e.msg.sender != 0);
}

function initialize_users(address user1, address user2, address user3) {
    // Validate user addresses:
    // - Must be non-zero addresses
    require(user1 != 0 && user2 != 0 && user3 != 0);
    // - Must be unique addresses
    require(user1 != user2 && user1 != user3 && user2 != user3);
    // Initialize targetUser to zero address
    require(targetUser == 0);
}

// Verify that total points always equal TOTAL_POINTS_PCT (100%)
rule users_points_sum_eq_total_points(env e, address user1, address user2, address user3) {
    // Set up initial state
    initialize_constructor(user1, user2, user3);
    initialize_env(e);
    initialize_users(user1, user2, user3);

    // Execute any method with any arguments
    method f;
    calldataarg args;
    f(e, args);

    // Calculate points for targetUser if it's not one of the initial users
    mathint targetUserPoints = targetUser != user1 && targetUser != user2 && targetUser != user3 ? ghostPoints[targetUser] : 0;
    
    // Assert total points remain constant at 100%
    assert(ghostPoints[user1] + ghostPoints[user2] + ghostPoints[user3] + targetUserPoints == TOTAL_POINTS_PCT());

    // All other addresses must have zero points
    assert(forall address user. user != user1 && user != user2 && user != user3 && user != targetUser
        => ghostPoints[user] == 0
    );
}
```

## Example 6 - Vesting Preclaim Abuse

Specification: a [`VestingExt`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/10-vesting-ext/VestingExt.sol) contract contains the same functionality as the previous `Vesting` contract plus an additional feature which lets users `preclaim` part of their token allocation, allowing users to get a limited amount of tokens before their vesting period is served.

When implementing the [fuzzer invariant](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-example-6-vesting-preclaim-abuse) I verified that the total `preclaimed` points is always less than or equal to the maximum preclaimable points (which is just the number of users multiplied by the maximum preclaim point amount per user):

```solidity
function property_total_preclaimed_lt_eq_max_preclaimable() public view returns(bool result) {
    result = totalPreclaimed <= MAX_PRECLAIMABLE;
}
```

However `alexzoid_eth` implemented a Certora [`rule`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/10-vesting-ext/certora.spec) which verifies `preclaimed` amounts are transferred at the same time as points:

```solidity
// solution provided by https://x.com/alexzoid_eth
methods {
    // `envfree` definitions to call functions without explicit `env`
    function allocations(address) external returns (uint24, uint8, bool, uint96) envfree;
    function getUserTokenAllocation(uint24) external returns (uint96) envfree;
    function getUserMaxPreclaimable(uint96) external returns (uint96) envfree;
}

// reusable helper functions to get data from underlying contract
function userPointsCVL(address user) returns uint24 {
    uint24 points; uint8 vestingWeeks; bool claimed; uint96 preclaimed;
    (points, vestingWeeks, claimed, preclaimed) = allocations(user);
    return points;
}
function userPreclaimedCVL(address user) returns uint96 {
    uint24 points; uint8 vestingWeeks; bool claimed; uint96 preclaimed;
    (points, vestingWeeks, claimed, preclaimed) = allocations(user);
    return preclaimed;
}
function userMaxPreclaimableCVL(address user) returns uint96 {
    uint96 maxPreclaimable = getUserMaxPreclaimable(getUserTokenAllocation(userPointsCVL(user)));
    return maxPreclaimable;
}

// when a user who has preclaimed transfers their points to another
// address, the preclaimed amount should transfer over to prevent
// gaming preclaim functionality by preclaiming more than allowed
rule preclaimedTransferred(env e, address targetUser, uint24 points) {
    // enforce address sanity checks
    require e.msg.sender != currentContract && targetUser != currentContract &&
            e.msg.sender != 0 && targetUser != 0;

    // enforce sender already preclaimed
    require userPreclaimedCVL(e.msg.sender) == userMaxPreclaimableCVL(e.msg.sender);
    // enforce receiver has no points and not preclaimed
    require userPreclaimedCVL(targetUser) == 0 && userPointsCVL(targetUser) == 0;

    // perform successful points transfer transaction
    transferPoints(e, targetUser, points);

    // assert both sender and receiver have preclaimed correctly
    // updated from their updated points 
    assert userPreclaimedCVL(e.msg.sender) == userMaxPreclaimableCVL(e.msg.sender);
    assert userPreclaimedCVL(targetUser)   == userMaxPreclaimableCVL(targetUser);
}
```

Given that there is no setup, handlers or other fuzzing “infrastructure”, this again is quite an elegant and concise solution.

## Example 7 - Operator Registry Corruption

Specification: an [`OperatorRegistry`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/11-op-reg/OperatorRegistry.sol) contract allows users to register as operators and receive an `operatorId` where the first `operatorId = 1` and subsequent ids are incremented.

The contract storage has multiple inter-related data structures which use both the user’s `address` and `operatorId` as keys in mappings to reference one another, enabling lookup of operator data by either `address` or `operatorId`. Users can also update their `address`.

I implemented the same invariant as the [fuzzer](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-example-7-operator-registry-corruption) but in a more elegant and concise Certora [`rule`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/11-op-reg/certora.spec), showing once again the great power of Certora’s domain-specific formal verification language especially when using parametric rules:

```solidity
// given two registered operators, there should be no f() that could
// corrupt the unique relationship between operator_id : operator_address
rule operator_addresses_have_unique_ids(address opAddr1, address opAddr2) {
    // enforce unique addresses in `operatorAddressToId` mapping
    require opAddr1 != opAddr2;

    uint128 op1AddrToId = currentContract.operatorAddressToId[opAddr1];
    uint128 op2AddrToId = currentContract.operatorAddressToId[opAddr2];

    // enforce valid and unique operator_ids in `operatorAddressToId` mapping
    require op1AddrToId != op2AddrToId && op1AddrToId > 0 && op2AddrToId > 0;

    // enforce matching addresses in `operatorIdToAddress` mapping
    require currentContract.operatorIdToAddress[op1AddrToId] == opAddr1 &&
            currentContract.operatorIdToAddress[op2AddrToId] == opAddr2;

    // perform any arbitrary successful transaction f()
    env e;
    method f;
    calldataarg args;
    f(e, args);

    // verify that no transaction exists which corrupts the uniqueness
    // property between operator_id : operator_address
    assert currentContract.operatorIdToAddress[op1AddrToId] !=
           currentContract.operatorIdToAddress[op2AddrToId];
}
```

Note again the use of `require` statements instructing Certora to create an initial valid state.

## Example 8 - Liquidate Denial Of Service

Specification: a [`LiquidateDos`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/12-liquidate-dos/LiquidateDos.sol) contract allows traders to enter multiple markets and have one open position in each market. Traders can also be liquidated:

* all open positions are accounted when determining if a trader is liquidatable
    
* if liquidated, all open positions are closed for the trader being liquidated
    
* liquidation should never fail with unexpected errors
    

Unfortunately at this time Certora can’t be used for Unexpected Denial Of Service checks as CVL does not return the reason for a revert - it only provides `lastReverted` and `lastHasThrown` which are both booleans (and `size` if using a `revert` opcode hook). Certora has confirmed in their discord that *“we have a plan to implement this feature in the prover”* so we will update once this feature is added.

## Example 9 - Stability Pool Drain

Specification: a [`StabilityPool`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/13-stability-pool/StabilityPool.sol) contract which:

* allows users to deposit `debtToken` which is used to pay down bad debt during liquidations
    
* in exchange `debtToken` depositors receive a share of `collateralToken` rewards from collateral seized during liquidations
    
* contains quite complicated logic to calculate the reward share `debtToken` depositors should receive
    
* must always remain solvent; the pool should always have sufficient `collateralToken` to pay out rewards owed to `debtToken` depositors
    

Using a `rule` construction I transformed the [invariant used in the fuzzer](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-example-9-stability-pool-drain) into a “scenario” which Certora was able to [solve](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/13-stability-pool/certora.spec):

```solidity
methods {
    // `envfree` definitions to call functions without explicit `env`
    function getDepositorCollateralGain(address) external returns (uint256) envfree;
}

// stability pool depositors should not be able to drain the stability
// pool; the stability pool should always hold enough collateral tokens
// to pay out rewards owed to depositors
rule stability_pool_solvent(address spDep1, address spDep2) {
    // enforce address sanity checks
    require spDep1 != spDep2 &&
            spDep1 != currentContract &&
            spDep1 != currentContract.debtToken &&
            spDep1 != currentContract.collateralToken &&
            spDep2 != currentContract &&
            spDep2 != currentContract.debtToken &&
            spDep2 != currentContract.collateralToken;

    // enforce neither user has active deposits or rewards
    require currentContract.accountDeposits[spDep1].amount     == 0 &&
            currentContract.accountDeposits[spDep1].timestamp  == 0 &&
            currentContract.depositSnapshots[spDep1].P         == 0 &&
            currentContract.depositSnapshots[spDep1].scale     == 0 &&
            currentContract.depositSnapshots[spDep1].epoch     == 0 &&
            currentContract.depositSums[spDep1]                == 0 &&
            currentContract.collateralGainsByDepositor[spDep1] == 0 &&
            currentContract.accountDeposits[spDep2].amount     == 0 &&
            currentContract.accountDeposits[spDep2].timestamp  == 0 &&
            currentContract.depositSnapshots[spDep2].P         == 0 &&
            currentContract.depositSnapshots[spDep2].scale     == 0 &&
            currentContract.depositSnapshots[spDep2].epoch     == 0 &&
            currentContract.depositSums[spDep2]                == 0 &&
            currentContract.collateralGainsByDepositor[spDep2] == 0;

    // enforce that both users have tokens to deposit into stability pool
    env e;
    uint256 user1DebtTokens = currentContract.debtToken.balanceOf(e, spDep1);
    uint256 user2DebtTokens = currentContract.debtToken.balanceOf(e, spDep2);
    require user1DebtTokens >= 1000000000000000000 && user2DebtTokens >= 1000000000000000000 &&
            user1DebtTokens == user2DebtTokens;
        
    // both users deposit their debt tokens into the stability pool
    env e1;
    require e1.msg.sender == spDep1;
    provideToSP(e1, user1DebtTokens);
    env e2;
    require e2.msg.sender == spDep2;
    provideToSP(e2, user2DebtTokens);

    // stability pool is used to offset debt from a liquidation
    uint256 debtTokensToOffset = require_uint256(user1DebtTokens + user2DebtTokens);
    uint256 seizedCollateral = debtTokensToOffset; // 1:1
    env e3;
    registerLiquidation(e3, debtTokensToOffset, seizedCollateral);

    require(currentContract.collateralToken.balanceOf(e, currentContract) == seizedCollateral);

    // enforce each user is owed same reward since they deposited the same
    uint256 rewardPerUser = getDepositorCollateralGain(spDep1);
    require rewardPerUser > 0;
    require rewardPerUser == getDepositorCollateralGain(spDep2);

    // enforce contract has enough reward tokens to pay both users
    require(currentContract.collateralToken.balanceOf(e, currentContract) >= require_uint256(rewardPerUser * 2));

    // first user withdraws their reward
    env e4;
    require e4.msg.sender == spDep1;
    claimCollateralGains(e4);

    // enforce contract has enough reward tokens to pay second user
    require(currentContract.collateralToken.balanceOf(e, currentContract) >= rewardPerUser);
    
    // first user perform any arbitrary successful transaction f()
    env e5;
    require e5.msg.sender == spDep1;
    method f;
    calldataarg args;
    f(e5, args);

    // second user withdraws their reward
    env e6;
    require e6.msg.sender == spDep2 &&
            e6.msg.value  == 0;
    claimCollateralGains@withrevert(e6);

    // verify first user was not able to do anything that would make
    // second user's withdrawal revert
    assert !lastReverted;
}
```

Note again the heavy usage of `require` statements to prevent Certora from breaking the assertion by generating an invalid state.

## Example 10 - Collateral Priority Corruption

Specification: a [`Priority`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/14-priority/Priority.sol) contract used in multi-collateral lending protocols:

* defines a liquidation priority order for collaterals
    
* when a liquidation occurs, the riskiest collaterals are liquidated first such that the borrower’s remaining collateral basket is more stable post-liquidation
    
* allows collaterals to be added and removed; adding always puts the new collateral at the end of the priority queue while removing preserves the existing order minus the removed element
    

Here I used a similar approach to Example #9, translating the [fuzzer invariant](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing#heading-example-10-collateral-priority-corruption) into a `rule` which describes a [scenario](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/14-priority/certora.spec) then verifies an assertion that Certora was able to break:

```solidity
methods {
    // `envfree` definitions to call functions without explicit `env`
    function getCollateralAtPriority(uint8) external returns(uint8)   envfree;
    function containsCollateral(uint8)      external returns(bool)    envfree;
    function numCollateral()                external returns(uint256) envfree;
}

// verify priority queue order is correctly maintained:
// - `addCollateral` adds new id to end of the queue
// - `removeCollateral` maintains existing order minus removed id
rule priority_order_correct() {
    // require no initial collateral to prevent HAVOC corrupting
    // EnumerableSet _positions -> _values references
    require numCollateral() == 0   && !containsCollateral(1) &&
            !containsCollateral(2) && !containsCollateral(3);

    // setup initial state with collateral_id order: 1,2,3 which ensures
    // EnumerableSet _positions -> _values references are correct
    env e1;
    addCollateral(e1, 1);
    addCollateral(e1, 2);
    addCollateral(e1, 3);

    // sanity check initial state
    assert numCollateral() == 3  && containsCollateral(1) &&
           containsCollateral(2) && containsCollateral(3);

    // sanity check initial order; this also verifies that
    // `addCollateral` worked as expected
    assert getCollateralAtPriority(0) == 1 &&
           getCollateralAtPriority(1) == 2 &&
           getCollateralAtPriority(2) == 3;

    // successfully remove first id 1
    removeCollateral(e1, 1);

    // verify it was removed and other ids still exist
    assert numCollateral() == 2  && !containsCollateral(1) &&
           containsCollateral(2) && containsCollateral(3);

    // assert existing order 2,3 preserved minus the removed first id 1
    assert getCollateralAtPriority(0) == 2 &&
           getCollateralAtPriority(1) == 3;
}
```

## Bonus - Certora Foundry Plug-In

Certora has experimental Foundry integration ([docs](https://docs.certora.com/en/latest/docs/cvl/foundry-integration.html), [examples](https://github.com/Certora/Examples/tree/master/FoundryIntegration)) that allows running Foundry stateless fuzz tests through Certora’s formal verification. Consider the function [`test_RarelyFalse`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/06-rarely-false/TargetFunctions.sol#L9-L25) containing a Chimera-style `t()` assertion which fails if `_rarelyFalse` returns `false`:

```solidity
uint256 constant private OFFSET = 1234;
uint256 constant private POW    = 80;
uint256 constant private LIMIT  = type(uint256).max - OFFSET;

// fuzzers call this function
function test_RarelyFalse(uint256 n) external {
    // input preconditions
    n = between(n, 1, LIMIT);

    // assertion to break
    t(_rarelyFalse(n + OFFSET, POW), "Should not be false");
}

// actual implementation to test
function _rarelyFalse(uint256 n, uint256 e) private pure returns(bool) {
    if(n % 2**e == 0) return false;
    return true;
}
```

At the current time of writing, none of the Fuzzers (Foundry/Echidna/Medusa) are able to find a case where `_rarelyFalse` returns `false` making the assertion in `test_RarelyFalse` fail - but Certora can find it very quickly without writing any extra code! First create the configuration file [`certora.conf`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/06-rarely-false/certora.conf) which along with the usual fields has an additional optional `foundry_tests_mode` set to `true`:

```solidity
{
  "files": [
    "test/06-rarely-false/RarelyFalseCryticToFoundry.sol"
  ],
  "verify": "RarelyFalseCryticToFoundry:test/06-rarely-false/certora.spec",
  "packages":[
        "@chimera=lib/chimera/src",
        "forge-std=lib/forge-std/src"
    ],
  "foundry_tests_mode": true
}
```

Then the [`certora.spec`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/06-rarely-false/certora.spec) file has this exact one line which is not specific at all to the test:

```solidity
use builtin rule verifyFoundryFuzzTests;
```

This simple setup allows Foundry stateless fuzz tests to be formally verified using Certora!

## Possible Improvements

Since Certora has created their own domain-specific language, it would be nice if it contained some “syntactic sugar” to make common patterns much easier and not error-prone to implement.

One common pattern is where a ghost variable is used to track the sum of all values in a mapping; this was used in the second solution to Example 5. Currently this pattern is quite cumbersome and error-prone to implement - it would be much nicer if some syntactic sugar could be provided that would turn it into a one liner like this:

```solidity
// sum all values in a mapping
ghost mathint sumOfPoints = always_sum(currentContract.allocations.points);

// sum values in a mapping for a given set of keys (here addresses)
ghost mathint sumOfPoints = always_sum(currentContract.balances, users);
```

Another potential improvement would be having `certoraRun` automagically read the library paths from the Hardhat/Foundry configuration so these wouldn’t need to be replicated inside the `.conf` file.

“Syntactic sugar” could condense the parameterized function calls eg:

```solidity
// call anything
env e;
method f;
calldataarg args;
f(e, args);

// call anything syntactic sugar
call_anything();

// call anything as `user`
env e5;
require e5.msg.sender == user;
method f;
calldataarg args;
f(e5, args);

// call anything as `user` syntactic sugar
call_anything(msg.sender == user);
```

## Conclusion

From the 10 fuzzing challenges based on simplified real-world vulnerabilities we were able to efficiently write 9 Certora specifications which correctly identified the same vulnerabilities, missing only challenge 8 due to CVL’s lack of support for returning the revert reason. In many cases the Certora solutions were more elegant and concise than the corresponding fuzzers since:

* there was no need to code setup or handlers
    
* due to Certora’s powerful features such as parametric rules
    

While it may sound daunting to learn Certora’s domain specific language, using the Certora lessons in [Updraft’s free course](https://updraft.cyfrin.io/courses/formal-verification) and the official [user guide](https://docs.certora.com/en/latest/docs/user-guide/index.html) I was able to learn enough CVL to write these solutions and this deep dive in only 7 days - if I can do it, then so can you!

Formal Verification using Certora is an effective tool which smart contract developers can use to identify a wide range of vulnerabilities prior to external audit. Certora’s generous free tier allows developers and auditors to [sign up for free](https://www.certora.com/signup?plan=prover&utm=updraft) and get a lot of free usage every month, more than sufficient for most small-medium size protocols.

2026 Update - RareSkills has published a great [Certora tutorial](https://rareskills.io/tutorials/certora-book)!