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
    • Examples
    • 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
  • Producing Positive Examples
  • 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
    • Introduction
    • Identifying timeout causes
    • Timeout prevention
    • Timeouts in Certora Prover - Theoretical Background
  • Checking Specifications
  • Troubleshooting
  • Frequently Asked Questions
  • Glossary
  • Contacting Certora
• The Certora Verification Language
  • Specification Files
    • Syntactic Conventions
  • Basic Syntax
    • Comments
    • Identifiers
    • Literals
  • Types
    • Syntax
    • Solidity Types
    • Additional CVL types
    • Conversions between CVL and Solidity types
  • Expressions
    • Syntax
    • Basic operations
    • String interpolation
    • Extended logical operations
    • Accessing fields and arrays
    • Contracts, method signatures and their properties
    • Special variables and fields
    • Calling contract functions
    • Comparing storage
    • Direct storage access
  • Statements
    • Syntax
    • Variable declarations
    • assert and require
    • satisfy statements
    • requireInvariant statements
    • Solidity-like statements
    • Function calls
    • havoc statements
  • Import and Use Statements
    • Syntax
  • Using Statements
    • Syntax
  • The Methods Block
    • Syntax
    • Methods entry patterns
    • envfree annotations
    • optional annotations
    • with(env e) clauses
    • Summaries
  • Rules
    • Syntax
    • Overview
    • Parametric rules
    • Filters
    • Multiple assertions
    • Rule descriptions
    • How rules are verified
  • Built-in Rules
    • Syntax
    • Bad loop detection — msgValueInLoopRule
    • Delegate call detection — hasDelegateCalls
    • Basic setup checks — sanity
    • Thorough complexity checks — deepSanity
    • Read-only reentrancy detection — viewReentrancy
  • Functions
    • Syntax
  • Invariants
    • Syntax
    • Overview
    • Invariants that revert
    • Preserved blocks
    • Filters
    • Writing an invariant as a rule
    • Invariants and induction
  • Uninterpreted Sorts
    • Syntax
  • Ghosts
    • Syntax
    • Declaring ghost variables
    • Using ghost variables
    • Initial state axioms
    • Ghost functions
  • Definitions
    • Syntax
  • Hooks
    • Syntax
  • EVM Opcode Hooks
    • Background
    • Hooking on opcodes
    • Hooking on raw reads and writes to storage
    • Missing instructions
    • Known inter-dependencies and common pitfalls
  • Changes Since CVL 1
    • Changes Introduced in CVL 2
    • CVL2 Migration Guide
    • Certora CLI 5.0 Changes
• The Certora Prover
  • 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
• Gambit: Mutation Generator for Solidity
  • Gambit: Mutant Generation for Solidity
    • Requirements
    • Installation
    • Usage
    • Examples
    • Configuration Files
    • Results Directory
    • CLI Options
    • Mutation Operators
  • Using Gambit with the Prover
    • Installations and Setup
    • Running the Mutation Verifier
    • Configurations
    • CLI Options
    • Troubleshooting
    • Visualization
• Equivalence Checking Using the Certora Prover
  • Installation
  • Example
  • Usage
    • Default mode
    • Configuration mode
• Old Documentation
  • Specification By Example
    • The Bank
    • The (Iterable) Map
  • The Anatomy of a Specification
    • Overview
    • CVL Functions
    • Ghosts
    • Ghost Functions
    • Storage 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
    • Grounding
  • 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