Contents Menu Expand Light mode Dark mode Auto light/dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content
Certora Prover Tutorials
Light Logo Dark Logo
Certora Prover Tutorials

Contents:

  • 1. Background and Prerequisites
    • 1.1. Background
    • 1.2. Introduction to predicate logic
    • 1.3. Introduction to formal verification
  • 2. Getting Started
    • 2.1. Installation and Setup
    • 2.2. Technology Overview
    • 2.3. ERC20 Example - Basics
    • 2.4. ERC20 Example - preconditions
    • 2.5. Parametric rules
    • 2.6. Using config files
    • 2.7. Vacuity
  • 3. Understanding violations
    • 3.1. Fixing ERC20 spec
    • 3.2. Borda count election
    • 3.3. Reward Challenge : Missing Spec bounty
  • 4. Invariants and Ghosts
    • 4.1. Simple invariants examples
    • 4.2. Basic exercises
    • 4.3. Preserved blocks
    • 4.4. Ghosts and hooks
    • 4.5. Ghost exercises
  • Index
Back to top

1.1. Background¶

Watch the following lecture by Certora’s CEO Prof. Mooly Sagiv: Auditing and Formal Verification - Better together

Next
1.2. Introduction to predicate logic
Previous
1. Background and Prerequisites
Copyright © 2023, Certora, Inc
Made with Sphinx and @pradyunsg's Furo