- Follow the installation instructions for the Certora Prover described in the following link: Installation of Certora Prover.
⚠️ Make sure to download solidity compiler versions 0.8.7, 0.8.0, 0.7.6, 0.7.5 and 0.7.0 for the first 2 lessons of the course. You will need additional solc versions in the future; so whenever a solc error will rise, make sure to have the compiler version that you need on your local machine, located in a directory added to PATH.
- Install VSCode if you don't already have it (can be found in their official website).
-
In the VSCode extensions/marketplace search for Certora Verification Language LSP and install it. This is an extension developed for supporting the spec language - the language in which we will be writing specifications. The extension supports syntax highlighting, autocompletion and more.
-
It is recommanded to install Certora IDE in the VSCode extensions/marketplace as well, to get an easy-to-use interface for running jobs.
-
It is also recommended to install the Ethereum Security Bundle by tintinweb on the VSCode extensions/marketplace, to get support for the Solidity contracts.
- Fork the Tutorials repository to your github account.
You can use the following link as a guide: Forking Repository On Github.
Clone your repository to your local machine so you'll have everything you need on your pc.
- Make sure to sync the forked repository daily in case any changes and fixes were made to the original repository. Use this link as a guide: Syncing A Forked Repository.
- Register to our Discourse Forum and consider and introduce yourself in the Introduction Thread.
ℹ️ The Certora team's recommends using VSCode as your main editor for writing specifications and browsing through contracts during the course. As part of the everyday work, you'll need convenient access to terminal, .spec editor - preferably with SLP extension, and a solidity editor - preferably with extension that has adequate support for reading and writing solidity code. You may, however, choose to work with any other (textual) editor of your choice or split the work between several editors, just know that the SLP is currently only supported through VSCode.
- Follow the ERC20Lesson1 instructions to learn the basics of operating the Certora Prover.
- Watch a lecture presented at Stanford Aug 2022 team by Dr. Michael George - Link. The lecture goes over the same examples from ERC20, explaining core concepts in more detail.
Writing the certoraRun command in a terminal every time we want to execute a run can be tiresome and uneasy on the eyes. Moreover, since a typical run of a single rule in real-life systems takes minutes to finish, we often work on 2 rules in parallel.
For that reason, we often write a shell script of the run command that includes all the settings and options we need for a run. There are 4 advantages for using a script:
- It is easier to read and sometimes can be more friendly to edit.
- It can save a large chunk of code that's stored in a known place, as opposed to a terminal command that can be pushed down the stack and disappear after intense use of the terminal.
- It can be uploaded to git or sent along with the specifications for others to use, instead of forcing them to write the command
- It allows a more advanced execution of run commands, e.g. running the exact same rule on every contract in a given directory (we will talk about sanity rule in the future).
- Follow the instructions on RunScriptExample to learn how to write run scripts, and how to execute the prover using scripts.
- Continue to the next lesson: Investigate Violations to exercise some more script writing and the art of understanding violations.
- Some of the lessons in the Tutorials require you to write a
.specfile containing your own rules for a given contract. Sometimes this can be quite challenging and if you get in trouble, you can have a look at the Solutions folder in the repository.