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
- Ghost Mapping Sums
- 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
- Induction Step for Transient Storage
- Writing an invariant as a rule
- Requiring Invariants
- 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
- Examples
- EVM opcode hooks
- Hook bodies
Transient Storage
Storage Layout Annotations
- Solidity and EIP-7201 namespace
- Table of Contents
- Storage Extension Flags
- How automatic generation works (high level)
- User-provided harnesses
- Quick example
- Troubleshooting
LSP Extension for VSCode
- CVL Formatter
Foundry Integration (Alpha)
- Usage (Automatic Setup)
- Usage (Manual Setup)
- Key differences vs. Foundry fuzz testing
- Known Limitations