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 premium access key as an environment variable
  • Step 4: Add the Solidity compiler (solc) executable’s folder to your PATH
  • Step 5 (for VS Code users): Install the Certora IDE Extension
• Prover Approximations
  • Loop Unrolling
  • Method Summarization
  • Harnessing
  • Modeling of Hashing in the Prover
• Techniques Used by Certora Prover
• Control Flow Splitting
• Storage and Memory Analysis
• Diagnostic Tools
  • TAC Reports
• Checking Specifications
  • Rule Sanity Checks
  • Bug Injection
  • Mutation Testing
• Certora Prover CLI
  • Verification
  • Linking
  • Certora Prover CLI Options
• Using the Certora Portal
  • Certora Verification Reports
  • Special Portal URLs
• Changelog
  • Prover Release Notes
  • Rules Report Release Notes
• New Certora dashboard login