Running the Certora Prover

The certoraRun utility simplifies the verification process by invoking the contract compiler (e.g., Solidity) and then sending the verification job to Certora’s servers.

The most commonly used command is:

certoraRun contractFile:contractName --verify contractName:specFile

If contractFile is named contractName.sol, the command can be further simplified to:

certoraRun contractFile --verify contractName:specFile

A concise summary of these options can be viewed by using:

certoraRun --help

Usage Example with ERC20 Contract

To demonstrate the usage, let’s consider an ERC20 contract named ERC20Fixed from the Certora Prover and CVL Examples Repository. The corresponding spec file is named ERC20Fixed.spec. Here is a rule from this spec:

from ERC20Fixed.spec

/// Transfer must move `amount` tokens from the caller's account to `recipient`
rule transferSpec {
    address sender; address recip; uint amount;

    env e;
    require e.msg.sender == sender;

    mathint balance_sender_before = balanceOf(sender);
    mathint balance_recip_before = balanceOf(recip);

    transfer(e, recip, amount);

    mathint balance_sender_after = balanceOf(sender);
    mathint balance_recip_after = balanceOf(recip);

    require sender != recip;

    assert balance_sender_after == balance_sender_before - amount,
        "transfer must decrease sender's balance by amount";

    assert balance_recip_after == balance_recip_before + amount,
        "transfer must increase recipient's balance by amount";
}

You can run the Certora Prover with the following command (from the /DEFI/ERC20/ folder in the repository):

certoraRun contracts/correct/ERC20Fixed.sol --verify ERC20Fixed:certora/specs/ERC20Fixed.spec

This command triggers a verification run on the ERC20 contract from the solidity file ERC20.sol, checking all rules in the specification file ERC20Fixed.spec.

Tip

You will need to use the correct version of the Solidity compiler. Either by

• using solc-select or having the compiler executable in your path (see Installing Solidity compiler),

• or by directing the certoraRun to the correct path using the solc argument.

Results

While running, the Prover will print various information to the console about the run. In the end, the output will look similar to this:

...

Job submitted to server

Follow your job at https://prover.certora.com
Once the job is completed, the results will be available at https://prover.certora.com/...

The output indicates that the Prover running the verification request, and it provides a link to view the results on the Certora platform.

Using Configuration (Conf) Files

For larger projects, managing the command line for Certora Prover can become complex. It is advisable to use configuration files (with a .conf extension) that hold the parameters and options for the Prover. These JSON5 configuration files simplify the process and enhance manageability. Refer to Configuration (Conf) Files for more detailed information.