2.6. Using config files

Introduction

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. Here is an example config file:

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

Note

In this case the working directory should be the same folder where both files are placed.

There are other reasons to prefer configuration files over directly using CLI:

  1. They are easier to read and sometimes friendlier to edit

  2. Since the configuration files are JSON5, they support comments

  3. We can include them in our git repository for version control

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.