2.1. Installation and Setup¶

Prover installation¶

Refer to the installation instructions for the Certora Prover described in: Installation of Certora Prover. Note you will need an appropriate Java version for the local type-checking to work, refer to the Installation of Certora Prover instructions.

You will also need solidity compiler versions 0.7.0, 0.8.0, 0.8.1, and 0.8.13 for this course. You can either download these to a folder included in your PATH, or use some other tool allowing to switch between solidity compilers, such as solc-select.

Recommended IDE¶

VSCode¶

If you are using VSCode we recommend using the following two VSCode extensions:

Certora Verification Language LSP: This extension is found in the VSCode extensions/marketplace. It provides syntactic support for the Certora Verification Language (CVL) - the language in which we will be writing specifications.
Ethereum Security Bundle: This extension, by tintinweb, is also found on the VSCode extensions/marketplace. It provides support for Solidity contracts.

Other IDEs¶

As part of the everyday work, you’ll need:

A convenient access to the terminal
An editor for CVL, preferably one with an appropriate extension providing syntax highlighting and an LSP (Language Server Protocol) for CVL
A solidity editor, also preferably with extension that has adequate support for editing solidity code.

We recommend using VSCode as it supports all the three requirements. You may however, choose to work with any other (textual) editor of your choice or split the work between several editors, however be aware that the LSP is currently only supported through VSCode.

Course Setup¶

Clone our Certora Tutorials Code repository, this includes all the code examples used in the tutorials. This code is updated periodically, so you may need to refresh your local copy over time.

Additional resources¶

Register to our Discord Server.
Use the #tutorials-questions channel to post questions and get answers.

Solutions¶

We’ve added solutions to some of the more difficult exercises. You can find them in the solutions folder.