- Watch a lecture by Dr. Chandrakana Nandi - Link On the mechanism of the Certora Verification Tool (Prover).
-
Follow the instructions on ScriptExercise2 to learn how to use additional frequently used flags.
-
Have a look at the shell scripts lying in this directory. They are real life examples for scripts that were used to run verifications on contracts of some well known actors in the Ethereum space.
These scripts flags and features that we still haven't gone through. Try to see if you recognize the parts that we did learned about, and use the--helpflag to read about additional flags you see if you are interested.
ℹ️ Writing shell scripts and executing shell commands are the way to operate the Prover at the moment. The Certora Development team is working on a GUI that facilitate generation of the shell scripts, displaying reports with extra useful information and many more helpful features.
- Have a brief look at the entry on CLI Options in the documentation.
This is where you'll go to learn about additional flags and options. Some of these can help you overcome problems, customize the output to your needs, and make your life much easier. We will introduce more specific flags in future lessons when using them help us solve problems.
- Continue to next lesson: Thinking Properties to learn what are systems' properties and how to think about them for the purpose of writing specifications.