1. Background and Prerequisites

The sections of this lesson are:

• Background – a video lecture giving background about the Certora Prover and its usefulness in auditing DeFi code.

• Introduction to predicate logic – provides a basic introduction to predicates, propositional logic and quantifiers. Feel free to skip if you are familiar with these concepts.

• Introduction to formal verification – provides a basic introduction to formal verification via an example.

Contents:

• 1.1. Background
• 1.2. Introduction to predicate logic
  • Propositional logic
  • Predicates
  • Quantifiers
  • Vacuity
  • Logical operators and quantifiers
  • Quiz
• 1.3. Introduction to formal verification
  • Finding a solution
  • Proving the solution is unique