CVL Language for Formal Verification

Preconditions

By adding preconditions, one can eliminate infeasible states and put constraints on values. The Rule totalSupplyAfterMintWithPrecondition is a copy of totalSupplyAfterMint with an additional constraint, shown in emphasis below:

/** @title Total supply after mint is at least the balance of the receiving account, with
 *  precondition.
 */
rule totalSupplyAfterMintWithPrecondition(address account, uint256 amount) {
    env e; 

    // Assume that in the current state before calling mint, the total supply of the 
    // system is at least the user balance.
    **uint256 userBalanceBefore =  balanceOf(account);**
    uint256 totalBefore = totalSupply();
    require totalBefore >= userBalanceBefore; 

    mint(e, account, amount);

    uint256 userBalanceAfter = balanceOf(account);
    uint256 totalAfter = totalSupply();

    // Verify that the total supply of the system is at least the current balance of the account.
    assert totalAfter >= userBalanceAfter, "total supply is less than a user's balance ";
}

The Prover will now assume that in the initial state, i.e. before calling mint(), the total supply is at least the user’s balance. Now run the rule totalSupplyAfterMintWithPrecondition:

**To note : Unlike Solidity, in CVL an uninitialized variable can have any value, though its possible values are constrained by CVL require statements in the rule. Additionally, CVL variables are immutable, so they cannot be changed in the course of the rule.

Mastering Parametric Rules in Certora Verification Language (CVL)

I'll guide you through creating parametric rules for smart contracts, same as the official tutorial, with a focus on the ERC20 token standard as our example.

What Are Parametric Rules?

Parametric rules allow you to verify properties across all functions in a contract simultaneously. Rather than writing separate rules for each function, you can write a single rule that automatically checks your property against every method.

This is particularly useful for invariants that should hold regardless of which function is called, such as:

Token supply conservation
Access control patterns
State transition validations

Basic Structure of a Parametric Rule

Here's the general structure of a parametric rule:

rule ruleName(method f, <additional parameters>) {
    // Setup - initial state capture

    // Execute any method in the contract
    env e;
    calldataarg args;
    f(e, args);

    // Verify properties after execution
    // assert <your property>;
}

The key components are:

method f parameter: represents any method in the contract that we can finetune later to verify a result
calldataarg args: a special type that can represent any argument structure
f(e, args): the actual execution of whatever method is being tested

Creating Your First Parametric Rule

Let's create a parametric rule to verify that only a token holder can increase their allowances in an ERC20 contract:

rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
    // 1. Capture the state before execution
    mathint allowance_before = allowance(holder, spender);

    // 2. Execute any method in the contract
    env e;
    calldataarg args;
    f(e, args);

    // 3. Capture the state after execution
    mathint allowance_after = allowance(holder, spender);

    // 4. Assert our property
    assert allowance_after > allowance_before => e.msg.sender == holder,
        "only the sender can change its own allowance";
}

This rule verifies that if any method increases a holder's allowance, then it must have been called by the holder themselves.

Filtering Methods with Selectors

Sometimes you want to make assertions about specific methods or exclude certain methods from your parametric rule. You can do this using the .selector property:

// Check if the method is approve()
f.selector == sig:approve(address, uint).selector

// Check if the method is transfer() OR transferFrom()
f.selector == sig:transfer(address, uint).selector ||
f.selector == sig:transferFrom(address, address, uint).selector

Let's enhance our rule to verify that only approve() and increaseAllowance() methods can increase allowances:

rule onlyApproveCanIncreaseAllowance(address holder, address spender, method f) {
    mathint allowance_before = allowance(holder, spender);

    env e;
    calldataarg args;
    f(e, args);

    mathint allowance_after = allowance(holder, spender);

    assert (
        allowance_after > allowance_before =>
        (
            f.selector == sig:approve(address, uint).selector ||
            f.selector == sig:increaseAllowance(address, uint).selector
        )
    ),
    "only approve and increaseAllowance can increase allowances";
}

Handling Exceptions for Specific Methods

Sometimes certain methods have legitimate reasons to break a rule. In these cases, you can exclude them from your verification:

rule conservesTotalSupply(method f) {
    // Skip mint and burn functions
    require f.selector != sig:mint(address, uint).selector;
    require f.selector != sig:burn(address, uint).selector;

    mathint totalSupply_before = totalSupply();

    env e;
    calldataarg args;
    f(e, args);

    mathint totalSupply_after = totalSupply();

    assert totalSupply_before == totalSupply_after,
        "total supply must remain constant for standard operations";
}

Config Files

For larger projects, the command line for running the Certora Prover can become large and cumbersome. It is therefore recommended to use configuration files instead. These are JSON5 files (with .conf extension) that hold the parameters and options for the Prover.

{
    "files": [
        "ERC20.sol"
    ],
    "verify": "ERC20:ERC20.spec",
    "wait_for_results": "all",
    "rule_sanity": "basic",
    // Note: json5 supports comments!
    "msg": "First run using .conf file"
}

This is a config file for running the ERC20.spec, and it is found in the same folder, in sample_conf.conf. Using this file we can run the Certora Prover by simply entering:

certoraRun sample_conf.conf

Some config file fields

files A list of the files containing the contracts needed. If a file contains several contracts and you wish to verify one of them, write it as contractFile:contractName.

verify This is the same as the --verify argument for the certoraRun script, so it accepts a string of the form <contract name>:<path to spec>.

wait_for_results If the value is "all", then the Prover will wait for the cloud job to complete, and display the log and results in the meantime.

solc Path to the solidity compiler, this is the same as the --solc argument for the certoraRun script.

msg The same as the --msg argument for the script.

rule_sanity Check rules for vacuity, triviality and similar conditions. Vacuity means the rule passes because there are no computation paths satisfying the requirements. See Vacuity for more information.

Triviality means the invariant always holds, even without the pre-condition. Possible values for rule_sanity are "none", "basic" and "advanced". See Rule Sanity Checks for more information.

Warning :Always use "rule_sanity": "basic" or "rule_sanity": "advanced" when running the Prover, as it is very easy to write vacuous rules without noticing.

Example of a vacuous rule :

rule simpleVacuousRule(uint256 x, uint256 y) {
    // Contradictory requirement
    require (x > y) && (y > x);
    assert false;  // Should always fail
}

Reverting Computation paths

By default, the Prover ignores computation paths that result in a revert. So, by default the Prover considers only those computation paths where all Solidity require statements are satisfied.

Moreover, any overflow or underflow paths are ignored (when using Solidity versions that revert on overflow and underflow).

To include computation paths that result in a revert, use the operator @withrevert when calling a Solidity function, e.g. someFunction**@withrevert(**args**)**. CVL has a builtin boolean variable lastReverted that is true if the last Solidity function called reverted (whether it used @withrevert or not).

Note that if the call someFunction**@withrevert(**args**)** does revert, its return value will be arbitrary, and all Solidity variables will also revert.

Learning Certora Prover (Part 2)