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: Install the relevant Solidity compiler versions
  • Step 5 (optional, for Vyper users): Install the Vyper compiler (vyper)
  • Step 6 (for VS Code users): Install the Certora Verification Language LSP
• 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
  • Configuration (Conf) Files
• Using the Certora Portal
  • Certora Verification Reports
  • Special Portal URLs
• Changelog
  • Prover Release Notes
  • Rules Report Release Notes