Certora Prover Documentation

Contents

• Certora Technology White Paper
  • Certora Tool Suite
  • Verification vs. Auditing
  • Verification vs. Testing
  • Experience to Date
    • Case Studies
  • Key Features
  • Design Principles
  • Technical Details
    • Formal Specification
    • Inductive Invariants
    • Rules
  • Verification via Constraint Solving
    • Boolean Satisfiability
    • Formal Verification by Reduction to Satisfiability
    • Beyond Booleans: SMT
    • Speeding Up Constraint Solving with Static Analysis
    • Modularity
  • The Certora Prover Architecture
  • Related Tools and Other Approaches
    • Unit Testing and Fuzzing
    • Traditional Static Analysis
    • Proof Assistants
  • Conclusions
• Certora User’s Guide
  • Introduction
  • Tutorial and Workshops
    • Tutorial
    • Stanford DeFi Security Summit
    • EthCC Paris
    • Aave Community Day
  • Getting Started
    • Installation
    • Project Layout
    • Running the Certora Prover
  • Specification By Example
  • Designing Good Specifications
    • Method Specifications
    • Variable Changes
    • Variable Relationships
    • State-Transition Systems
    • Risk Assessment
    • Mathematical Properties
  • Specification Design Patterns
    • Tracking Sums
    • Partially Parametric Rules
    • Listing Safe Assumptions
    • Writing State-Based Invariants
    • General Rules
  • Working with Multiple Contracts
    • Example protocol
    • Handling unresolved method calls
    • Working with known contracts
    • Working with unknown contracts
    • Conclusion
  • Managing Timeouts
    • What causes timeouts?
    • The complexity check
    • Summarizing complex functions
    • Flags for tuning the Prover
  • Checking specifications
  • Troubleshooting
  • Frequently Asked Questions
  • Glossary
• The Certora Verification Language
  • Specification Files
  • Syntactic conventions
  • Common Syntactic Elements
    • Basic Syntax
    • Types
    • Mathematical Operations
    • Expressions
    • Statements
  • Specification File Contents
    • Pragmas
    • Import and Use Statements
    • Using statements
    • The Methods Block
    • Events
    • Rules
    • Built-in Rules
    • Functions
    • Invariants
    • Uninterpreted Sorts
    • Ghosts
    • Definitions
    • Hooks
• The Certora Prover
  • Introduction
  • Installation
    • Step 1: prerequisites
    • Step 2: Install the Certora Prover package
    • 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
  • 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
    • Prod version March 21, 2022
    • Prod version March 6, 2022 [MAJOR]
    • Prod version February 24, 2022
    • Prod version February 10, 2022
    • Prod version January 30, 2022
    • Prod version January 3rd, 2022
    • Prod version January 1st, 2022
    • Prod version December 19, 2021
    • Prod version December 12, 2021
    • Prod version December 4, 2021
    • Prod version November 16, 2021
    • Prod version November 15, 2021
    • Prod version November 7, 2021
    • Prod version October 3, 2021
    • Prod version August 29th, 2021
    • Prod version August 8th, 2021
    • Prod version July 18, 2021
    • Prod version July 17, 2021
    • Prod version July 12, 2021
    • Prod version June 14th, 2021
    • Prod version June 13th, 2021
    • Prod version May 30th, 2021
• Gambit: Mutation Generator for Solidity
  • Generating Mutations
    • Installing Gambit
    • Usage
    • Mutation Types
  • Using Gambit with the Prover
    • Installations and Setup
    • Running the Mutation Verifier
    • Configuration
    • Visualization
• Old Documentation
  • Specification By Example
    • The Bank
    • The (Iterable) Map
  • The Anatomy of a Specification
    • Overview
    • CVL Functions
    • Ghosts
    • Ghost Functions
    • Hooks
    • Definitions
    • Multicontract Hooks
    • A Complete Example
    • Syntax Update: Ghost Variables and Ghost Mappings
  • Advanced Subjects
    • Method declarations
    • Summarizing Solidity Functions
    • Internal Function Summaries
    • More Expressive Summaries
    • Multicontract
    • Linking Contracts
    • Approximation
    • Advanced Debugging
  • Best Practices
    • When to use the environment argument?
  • Common Pitfalls
    • Vacuity
    • lastReverted updates
  • Assert splitting
    • How the sub rules are generated
    • What if I have an assert command within an if-else statement
    • Report
  • Troubleshooting
    • Timeouts
    • Errors
    • Understanding counter-examples