Certora tutorial lecture notes

Contents:

• Getting started with the Certora Prover
  • Simple Voting Contract
  • First spec
  • First conf
  • Exercises
• Inductive Properties
  • Task 3: Write a rule to verify the property
  • Inductive Invariants
  • Another bug
  • Exercises
• A minimal token
  • Minimal token code
  • Invariants
• Power voting
  • Revisiting the Voting Contract
  • Spec
  • Exercises
• Flashloan exploit
  • Adding flashloan capability
  • Creating a borrower
  • Revisiting tokenSolvency
  • Exercises

Useful links

• Code repository: https://github.com/Certora/basic-presentation.

• Prover installation instructions

• Certora Prover documentation

• Certora Prover tutorials

Indices and tables

• Search Page