Step 1: Prerequisites
Python3.5 and later
Java 11 and later
Solidity compiler (ideally v0.5 and up)
Step 2: Install the Certora Prover package
Step 3: [Optional: if you received a key] Set access key as an environment variable
The Certora Prover requires a valid key when running the tool. For ease of use, it is recommended to set it in an environment variable called
(value is the key provided by the Certora team.)
Step 4: Add the solidity compiler (solc) executable's folder to your PATH
(How to do this depends on your operating system.)
Step 5: Download examples
It's highly recommended to first try out the tool on basic examples, such as those available in this repository. The repository also includes syntax highlighting of specification files for common editors (VSCode, notepad++).
Running the Certora Prover
We start with a simple example. After cloning the examples repository, run:
Windows users should run the tool with
The above command will trigger the verification of the contract
Counter located in the Solidity file
InvertibleBroken.sol, using the rules defined in the specification file
Counter.spec. After authorizing the request based on the provided access key, the tool sends the job to Certora's server. Messages will be printed to the command line, informing about its progress. Note that even if you interrupt the process, the job continues to process. An email notification is sent when the verification is complete, containing links to the results. If the CLI tool is not interrupted, the output will also contain the links to the results:
Follow this link to view the results. A verification report is an HTML file presenting a table with all the spec file rules. Each formally proved rule has a green color, and violated rules are colored red. The report will also include the call trace and the arguments that led to the violation. In this example, the Certora Prover finds a violation of the
monotone rule. Click the rule to see the call trace and try to figure out the reason.
Need some help? Try to run another verification on
CounterFixed.sol and see the difference.
An explanation of the results is briefly described here. To find out more about how to run the tool, see Certora Prover CLI Options.
Congratulations! You have just completed a verification using Certora Prover.