# Running the Certora Prover

Basic examples are available in this repository. The repository also includes syntax highlighting of specification files for common editors (VSCode, notepad++).

git clone [email protected]:Certora/CertoraProverSupplementary.git


We start with a simple example. After cloning the examples repository, open terminal and move to the specified directory:

cd CertoraProverSupplementary/Examples/Simple


Then run the following command to specify a verification job:

certoraRun CounterBroken.sol:Counter --verify Counter:Counter.spec


Note

Windows users should run the tool with certoraRun.exe

The above command will trigger the verification of the contract Counter located in the Solidity file CounterBroken.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:

Status page: https://prover.certora.com/jobStatus/...?anonymousKey={anonymousKey}
Verification report: https://prover.certora.com/output/...?anonymousKey={anonymousKey}
Full report: https://prover.certora.com/zipOutput/...?anonymousKey={anonymousKey}


A verification report is an HTML file presenting a table with all the spec file rules. Each formally proved rule has a green color. 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.