At DeFi Security Summit 2024 I presented a workshop on how smart contract developers can use invariant fuzz testing to find high severity issues 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” 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 (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!

Special thanks also to:

Updraft Assembly & Formal Verification Course which is free and great for learning Certora!
alexzoid_eth who provided invaluable assistance improving some of the solutions
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 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. 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” 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 file with some basic information - the contracts we are testing and optional Certora flags
write a .spec specification 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 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 statements which are the actual properties we are trying to break
invariant 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 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 and opcode hooks - keep the user guide 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 and 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 and Lender. 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:

{
  "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:

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

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 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 in our Certora specification:

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 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. The certora.conf looks like this:

{
  "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 we implemented the two fuzzer invariants using one rule per invariant which worked very well:

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 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 in the constructor ensuring that all points are allocated:

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 that achieves the same outcome:

// 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 also implemented another rule which uses the same idea as the fuzzer invariant:

// 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 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 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):

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

However alexzoid_eth implemented a Certora rule which verifies preclaimed amounts are transferred at the same time as points:

// 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 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 but in a more elegant and concise Certora rule, showing once again the great power of Certora’s domain-specific formal verification language especially when using parametric rules:

// 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 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 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 into a “scenario” which Certora was able to solve:

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 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 into a rule which describes a scenario then verifies an assertion that Certora was able to break:

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, examples) that allows running Foundry stateless fuzz tests through Certora’s formal verification. Consider the function test_RarelyFalse containing a Chimera-style t() assertion which fails if _rarelyFalse returns false:

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 which along with the usual fields has an additional optional foundry_tests_mode set to true:

{
  "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 file has this exact one line which is not specific at all to the test:

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:

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

// 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 and the official user guide 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 and get a lot of free usage every month, more than sufficient for most small-medium size protocols.

Find Highs Before External Auditors Using Certora Formal Verification

Table of contents

Invariant Fuzz Testing vs Formal Verification

Solidity vs Certora Verification Language (CVL)

Fuzz Locally vs Cloud Formal Verification

Fuzz Setup vs Formal Verification Relationships

Fuzz Invariant vs Certora `rule` and `invariant`

Fuzz Cheat Codes vs Certora `env`

Additional Certora Features

Example 1 - Flash Loan Denial Of Service

Example 2 - Reward Distribution Stuck

Example 3 - Voting Power Destruction

Example 4 - Token Sale Drain

Example 5 - Vesting Points Increase

Example 6 - Vesting Preclaim Abuse

Example 7 - Operator Registry Corruption

Example 8 - Liquidate Denial Of Service

Example 9 - Stability Pool Drain

Example 10 - Collateral Priority Corruption

Bonus - Certora Foundry Plug-In

Possible Improvements

Conclusion

Subscribe to my newsletter

Dacian

Dacian

Find Highs Before External Auditors Using Certora Formal Verification

Table of contents

Invariant Fuzz Testing vs Formal Verification

Solidity vs Certora Verification Language (CVL)

Fuzz Locally vs Cloud Formal Verification

Fuzz Setup vs Formal Verification Relationships

Fuzz Invariant vs Certora rule and invariant

Fuzz Cheat Codes vs Certora env

Additional Certora Features

Example 1 - Flash Loan Denial Of Service

Example 2 - Reward Distribution Stuck

Example 3 - Voting Power Destruction

Example 4 - Token Sale Drain

Example 5 - Vesting Points Increase

Example 6 - Vesting Preclaim Abuse

Example 7 - Operator Registry Corruption

Example 8 - Liquidate Denial Of Service

Example 9 - Stability Pool Drain

Example 10 - Collateral Priority Corruption

Bonus - Certora Foundry Plug-In

Possible Improvements

Conclusion

Subscribe to my newsletter

Dacian

Dacian

Fuzz Invariant vs Certora `rule` and `invariant`

Fuzz Cheat Codes vs Certora `env`