The Certora Prover

Note

The reference manual is currently being heavily edited and reorganized. Where possible, we have included links to the best existing documentation for each topic.

Contents

• Introduction
• Installation
  • Step 1: Prerequisites
  • Step 2: Install the Certora Prover package
  • Installing the beta version (optional)
  • Step 3: Set the personal access key as an environment variable
  • Step 4 (for GitHub users): Configure Syntax Highlighting
• Prover Approximations
  • Loop Unrolling
  • Method Summarization
  • Harnessing
  • Modeling of Hashing in the Certora Prover
  • Quantifier Grounding
• Techniques Used by the Certora Prover
  • Control flow splitting
  • Analysis of EVM storage and EVM memory
• Diagnostic Tools
  • TAC Reports
• Checking Specifications
  • Rule Sanity Checks
  • Coverage Info
  • Bug Injection
  • Mutation Testing
• Certora Prover CLI
  • CLI Options
  • Most frequently used options
  • Options affecting the type of verification run
  • Options that control the Solidity compiler
  • Options regarding source code loops
  • Options regarding summarization
  • Options regarding hashing of unbounded data
  • Options that help reduce the running time
  • Options to set addresses and link contracts
  • Options for job metadata and dashboard filtering
  • Options for controlling contract creation
  • Version options
  • Conf file options
  • Advanced options
  • Configuration (Conf) Files
• Using the Certora Portal
  • Certora Verification Reports
  • Special Portal URLs
• Changelogs
  • Prover Release Notes
  • GUI Release Notes