This course is designed to get you started with Certora's Software as a Service called Certora Prover.
The Certora Prover is a tool with an underlying technology based on 30 years of research in Formal Verification. It allows checking at compile-time whether all executions of a Smart Contract are fulfilling a set of pre-defined specifications. At the moment, the Certora Prover can run verifications on any computer program that can be compiled using EVM.
The course will teach you how to think about system properties through a "rule writer"'s goggles, write specifications in Certora's spec language, and use the Certora Prover technology to verify your specifications or find bugs. We will guide you through the many features of the Certora Prover, basic workflow for approaching a verification job, and best practices that the Certora team has developed.
During the course, you will read articles and documentations, watch videos, and witness examples of real-life systems. All of these will be associated with the Ethereum blockchain and framework. The contracts are written in Solidity.
The course is built as 17 lessons, each tries to address exactly one subject/feature. The course will be available on Certora's Github as a repository containing Lessons 1-17. It contains README files that provide everything you need to complete the tasks and exercises. You may fork this repository or open a branch to push your solutions as you advance. < Nurit : maybe> Some exercises will be checked by yourself, some by teammates, and some directly by the Certora team.
The course caters to absolute beginners in Formal Verification. However, we do assume a certain level of proficiency in some areas:
-
A basic understanding of the Ethereum framework (events, gas, msg. , block. , etc.) and the Solidity language (the ability to read code is more important than writing).
-
Familiarity with some basic and standard protocol contracts such as ERC20.
-
We will use propositional logic to express rules and invariants about the systems we verify. Therefore, we expect basic familiarity with logic - signs, terms, and definitions.
The Certora team will be available for questions and help with the exercises daily on various platforms:
-
Discourse Forum - here, you can start a thread on any subject related to the course, discuss with other users, and browse through similar questions that have already been and answered.
-
Direct questions through to the Certora team - a zoom meeting link and hours will be published.
We strongly believe in the mantra "There's no such thing as a stupid question". Therefore, we encourage discussions and knowledge sharing between fellow users. We invite you to get the most out of the course by utilizing all of the platforms and resources supplied here to ask questions and discuss the course's subjects.