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
- Basic Syntax
- Types
- Expressions
- Statements
- Import and Use Statements
- Using Statements
- The Methods Block
- Rules
- Built-in Rules
- Functions
- Invariants
- Uninterpreted Sorts
- Ghosts
- Definitions
- Hooks
- Transient Storage
- Foundry Integration (Alpha)
- Usage
- Key differences vs. Foundry fuzz testing
- Known Limitations