Certora Prover Documentation
latest
Contents
Certora User’s Guide
The Certora Verification Language
The Certora Prover
Gambit: Mutation Generator for Solidity
Additional information
The Certora Equivalence Checker
Certora Technology White Paper
Old Documentation
Specification By Example
The Anatomy of a Specification
Overview
CVL Functions
Ghosts
Ghost Functions
Storage Hooks
A Complete Example
Syntax Update: Ghost Variables and Ghost Mappings
Advanced Subjects
Best Practices
Common Pitfalls
Assert splitting
Troubleshooting
Index
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
Two State Context
Havoc Assuming
A Hook that Modifies Ghost State
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