Installation
Step 1: prerequisites
Python3.5 or newer
Check your Python3 version by executing the following command on the terminal:
python3 --version
If the version is < 3.5, 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)
If you use a specific version of Solidity in your contract, download the needed Solidity compiler from the official Solidity repository on GitHub. Make sure to place all the compilers that you download 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
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:
Windows
So far we haven’t encountered any warnings at installation that’s needed to be resolved to use the tool freely, however it doesn’t mean that you won’t encounter one.
If you do encounter a warning try the following solutions in descending order:
Follow the warning’s instructions.
If you do not understand the warning and don’t know how to fix it, try to compare it to the warning of the other OS and follow their instructions.
The warnings in the other OS suggest to add the installation folder to the PATH.
To get the location of the
certora-cli
installation re-execute oncmd
:pip install certora-cli
Contact the Certora team.
Please also share the warning with us so we could write a walkthrough for fixing it.
macOS
Caution
The script certoraRun
is installed in
‘/Users/user_name/Library/Python/3.8/bin’ which is not on PATH. Consider
adding this directory to PATH
Open a terminal and move to the
etc/paths.d
directory from root:cd /etc/paths.d
Use root privileges to create a file with an informative name such as
PythonForProver
, and open it with your favorite text editor:sudo nano PythonForProver
Write the specified path from the warning:
/specified/path/in/warning
If needed, more than one path can be added on a single file, just separate the path with a colon (
:
).Quit the terminal to load the new addition to
$PATH
, and reopen to check that the$PATH
was updated correctly:echo $PATH
Linux
Caution
Known warning - “The script certoraRun
is installed in ‘/home/user_name/.local/bin
’ which is not on PATH. Consider adding this directory to PATH”
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, add to
PATH="..."
the specified path from the warning. To add an additional path just separate with a colon (:
) :PATH="$PATH:/specified/path/in/warning"
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 changes to the
$PATH
by executing the script:source .profile
Step 4: Add the Solidity compiler (solc
) executable’s folder to your PATH
Windows
The following instructions are for Windows 11; for other versions of Windows the instructions might slightly differ.
Press
"Windows key" + x
to access the Power User Task Menu.In the Power User Task Menu, select the System option.
In the System window, scroll to the bottom and click the About option.
In the System > About window, click the Advanced system settings link at the bottom of the Device specifications section.
In the System Properties window, click the Advanced tab, then click the Environment Variables button near the bottom of that tab.
In the Environment Variables window, highlight the Path variable in the System variables section and click the Edit button.
Add the full path to the directory that contains the
solc
executables, e.g.:C:\full\path\to\solc\executable\folder
Quit and reopen all opened terminals for the change to take effect in the terminals.
You can check that the variable was set correctly by running the following in the cmd terminal:
echo %PATH%
macOS
Open a terminal and move to the
etc/paths.d
directory from root:cd /etc/paths.d
Use root privileges to create a file with an informative name such as
SolidityCertoraProver
, and open it with your favorite text editor:sudo nano SolidityCertoraProver
Write the full path to the directory that contains the
solc
executables:/full/path/to/solc/executable/folder
If needed, more than one path can be added on a single file, just separate the path with colon a (
:
).
Quit the terminal to load the new addition to
$PATH
, and reopen to check that the$PATH
was updated correctly:echo $PATH
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, add to
PATH="..."
the full path to the directory that contains thesolc
executables. To add an additional path just separate with a colon (:
) :PATH="$PATH:/full/path/to/solc/executable/folder"
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 changes to the
$PATH
by executing the script:source .profile
Step 5 (for VS Code users): Install the Certora IDE Extension
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 IDE Extension for that program.
To install VS Code, follow the platform specific instructions found on the Visual Studio Code website.
Once VS Code is installed, search for “Certora IDE” in VS Code’s extension pane or navigate there directly and follow the prompts to install the extension.
Instructions on how to use the Certora IDE extension are available directly from the extension’s marketplace page.
Congratulations! You have just completed Certora Prover’s installation and setup.
Caution
We strongly recommend trying the tool on basic examples to verify correct installation. See Running the Certora Prover for a detailed walkthrough.