Installation

Step 1: prerequisites

Python3.8.16 or newer

Check your Python3 version by executing the following command on the terminal:

python3 --version

If the version is < 3.8.16, follow the Python installation guide to upgrade.

Java Development Kit (JDK) 11 or newer

Check your Java version by executing the following command on the terminal:

java -version

If the version is < 11, download and install Java version 11 or later from Oracle.

Solidity compiler (ideally v0.5 and up)

We recommend using solc-select to download and switch between Solidity compiler versions.
You can also download the Solidity compiler binaries from the official Solidity repository on GitHub. It is best to place all the solc binaries in the same path.
Certora employees can clone the CVT_Executables repository suitable for their OS from GitHub.

Step 2: Install the Certora Prover package

Tip

It is always recommended to use a Python virtual environment, such as venv or virtualenv, when installing a Python package.

Execute the following command at the terminal to install the Prover:

pip3 install certora-cli

Caution

Note that the terminal may prompt you with a warning that some files, e.g. python3.x, are not included in the PATH, and should be added. Add these files to PATH to avoid errors.

The following section presents some, but maybe not all, possible warnings that can arise during installation and how to deal with them:

Installing the beta version (optional)

If you wish to install a pre-release version, you can do so by installing certora-cli-beta instead of certora-cli. We do not recommend having both packages installed simultaneously, so you should remove the certora-cli package before installing certora-cli-beta:

pip uninstall certora-cli
pip install certora-cli-beta

If you wish to easily switch between the beta and the production versions, you can use a python virtual environment:

pip install virtualenv
virtualenv certora-beta
source certora-beta/bin/activate
pip3 install certora-cli-beta

You can then switch to the standard CVL release by running deactivate, and back to the beta release using certora-beta/bin/activate.

Step 3: Set the personal access key as an environment variable

The Certora Prover requires a personal access key. You can get a free personal access key by registering on the Certora website.

Before running the Prover, you should register your access key as a system variable. To do so on macOS or Linux machines, execute the following command on the terminal:

export CERTORAKEY=<personal_access_key>

This command sets a temporary variable that will be unset once the terminal is closed. We recommended storing the access key in an environment variable named CERTORAKEY. This way, you will no longer need to execute the above command whenever you open a terminal. To set an environment variable permanently, follow the next steps:

macOS

Open a terminal and make sure you’re in the home directory:
```
cd ~
```
Create a file with the name .zshenv and open it with your favorite text editor:
```
nano .zshenv
```
Write the export command from the beginning of step 3, save and quit (ctrl+x on nano).
You can make sure that the file was created correctly by seeing it listed on the directory or by opening it again with the text editor:
```
ls -a
```
OR
```
nano .zshenv
```
Make sure to apply the environment variable you’ve just created by executing the script:
```
source .zshenv
```

When running the Certora Prover in the Visual Studio Code Extension, you may need to restart VSCode or your computer.

Linux

Open a terminal and make sure you’re in the home directory:
```
cd ~
```
open the .profile file with your favorite text editor:
```
nano .profile
```
At the bottom of the file, under the PATH="..." insert the export command from the beginning of step 3, save and quit (ctrl+x on nano).
You can make sure that the file was modified correctly by opening it again with the text editor:
```
nano .profile
```
Make sure to apply the environment variable you’ve just created by executing the script:
```
source .profile
```

Step 4: Install the relevant Solidity compiler versions

The Solidity compiler (solc) is a verification requirement. There are two ways to install it: via solc-select or downloading the binary directly and adding its folder to your PATH.

Using `solc-select`

solc-select instructions

Open a terminal and install solc-select via pip:
```
pip install solc-select
```
Download the required compiler version. For example, if you want to install version 0.8.0, run:
```
solc-select install 0.8.0
```
Set solc to point to the required compiler version. For example:
```
solc-select use 0.8.0
```

Download binaries

You can download the solc binaries directly from Solidity’s release page on GitHub.

To run the Prover, you may find it useful to add the solc executables folder to your PATH. This way you will not need to provide the Prover with the full path to the solc executables folder every time.

Step 5 (optional, for Vyper users): Install the Vyper compiler (`vyper`)

Vyper is an EVM compatible Pythonic smart contract language. Since the Certora Prover operates on the bytecode, it can be applied to any source-level language that compiles to EVM bytecode. We recommend to install Vyper either from PyPi (i.e., pip install vyper) or to get a binary executable for the desired version.

Step 6 (for VS Code users): Install the Certora Verification Language LSP

All users of the Certora Prover can access the tool using the command line interface, or CLI. Those who use Microsoft’s Visual Studio Code editor (VS Code) also have the option of using the Certora Verification Language LSP. This will provide both syntax checking and syntax highlighting for CVL.

Congratulations! You have just completed Certora Prover’s installation and setup.