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

Certora Prover TutorialsΒΆ

Welcome to the tutorials for the Certora Prover. This will teach you how to use the Certora Prover to guarantee security properties of EVM smart contracts written in the Solidity language.

There is a separate tutorial for learning Certora Sunbeam for securing Soroban smart contracts written in Rust.

Contents:

  • 1. Background and Prerequisites
  • 2. Getting Started
  • 3. Understanding violations
  • 4. Invariants and Ghosts
Next
1. Background and Prerequisites
Copyright © 2023, Certora, Inc
Made with Sphinx and @pradyunsg's Furo