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

    "files": [
    "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


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#


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.


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>.


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.


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


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


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.


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