Certora Prover Documentation
latest
Contents
Certora Technology White Paper
Certora User’s Guide
The Certora Verification Language
The Certora Prover
Gambit: Mutation Generator for Solidity
Equivalence Checking Using the Certora Prover
Old Documentation
Specification By Example
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
Best Practices
Common Pitfalls
Assert splitting
Troubleshooting
Certora Prover Documentation
»
Old Documentation
»
The Anatomy of a Specification
Edit on GitHub
The Anatomy of a Specification
Overview
CVL Functions
Syntax
Using a CVL Function
Ghosts
What are ghosts?
A Simple Bank Example
Ghost Functions
Uninterpreted Sorts
Uninterpreted Functions
Axioms for Uninterpreted Functions
Initial Axioms for Uninterpreted Functions
Storage Hooks
Motivation
Program State
The Anatomy of a Hook
Hook Patterns
Sload
and
Sstore
Slot Patterns
Struct Patterns
Structs in Static Slots
Structs inside Mappings or Arrays
Manually Unpacking Structs
Putting it Together
The Body of a Hook
Two State Context
Havoc Assuming
A Hook that Modifies Ghost State
Definitions
Syntax
Basic Definitions
Advanced Definitions
Include an Application of Another Definition.
Reference Ghost Functions
Multicontract Hooks
A Complete Example
A Contract Implementing a Linked List
A Spec Using a Ghost to Compute Reachability
Syntax Update: Ghost Variables and Ghost Mappings
Variable-style declarations
Variable-style access
Mapping-style updates
Read the Docs
v: latest
Versions
latest
cvl1
Downloads
On Read the Docs
Project Home
Builds