The Certora Verification Language

The Certora Verification Language (often abbreviated CVL) is the language used to write specifications for smart contracts. This chapter describes the syntax and semantics of CVL Specifications.

• 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
  • Struct Comparison
  • 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
  • Built-in Functions
• Statements
  • Syntax
  • Variable declarations
  • assert and require
  • satisfy statements
  • requireInvariant statements
  • Havoc Statements
  • Solidity-like Statements
• Import and Use Statements
  • Examples
  • Syntax
• Using Statements
  • Examples
  • 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
  • Examples
  • Using CVL functions
• Invariants
  • Syntax
  • Overview
  • Invariants that revert
  • Preserved blocks
  • Filters
  • Writing an invariant as a rule
  • Invariants and induction
• Uninterpreted Sorts
  • Syntax for Uninterpreted Sorts
  • Example Usage
  • Using Uninterpreted Sorts with Ghosts
• Ghosts
  • Syntax
  • Declaring ghost variables
  • Ghost Functions
  • Restrictions on ghost definitions
  • Using ghost variables
  • Ghost axioms
  • Restrictions on ghost axioms
  • Ghosts vs. persistent ghosts
• Definitions
  • Basic Usage
  • Advanced Functionality
  • Filter Example
  • Syntax
• Hooks
  • Syntax
  • Examples
  • Load and store hooks
  • EVM opcode hooks
  • Hook bodies
• Transient Storage

Changes Since CVL 1

• Changes Introduced in CVL 2
  • Superficial syntax changes
  • Changes to methods block entries
  • Changes to integer types
  • Changes to the fallback function
  • Removed features
  • Changes to the Command Line Interface (CLI)
• CVL2 Migration Guide
  • Step 0: Install CVL 2
  • Step 1: Skim CVL 2 changes
  • Step 2: Run the migration script
  • Step 3: Fix type errors
  • Step 4: Review your methods blocks
  • Step 5: Profit!
• Certora CLI 5.0 Changes
  • Exhaustive parametric rules
  • Disallow calls to contract functions in quantified expressions
  • Method variable restrictions
  • New DELETE summary syntax
  • CLI changes: New Parametric Contracts Attribute
  • CLI changes: End of CVL1 Deprecation period