Warning

This page was created from a pull request (#74).

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
  • 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
    • What causes timeouts?
    • Summarizing complex functions
    • Library-based systems
    • Flags for tuning the Prover
  • Checking specifications
  • Troubleshooting
  • Frequently Asked Questions
  • Glossary
  • Contacting Certora
• 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
    • EVM (Ethereum Virtual Machine) Opcode Hooks
  • CVL Version 2
    • Changes introduced in CVL 2
    • Migration guide
• 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
  • 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
  • Release Notes
    • 4.5.1 (July 15, 2023)
    • 4.3.1 (July 2, 2023)
    • 4.0.5 (June 7, 2023) CVL 2
  • CallResolutionTable
    • Attributes
    • The Callee
    • Comments
• Gambit: Mutation Generator for Solidity
  • Mutant Generation
    • 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