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 Bank
The (Iterable) Map
The Anatomy of a Specification
Advanced Subjects
Best Practices
Common Pitfalls
Assert splitting
Troubleshooting
Certora Prover Documentation
»
Old Documentation
»
Specification By Example
Edit on GitHub
Specification By Example
The Bank
Rules in the Certora Verification Language
Parametric rules
Invariants
Declaring functions used in the invariant
envfree
functions
Understanding the results of the Certora Prover
The (Iterable) Map
Overview
A Simple Map
The code
Writing specs
Generalized unit tests
Revert conditions
Inverses
The IterableMap Contract
Adding iteration
A soft introduction to ghosts
Verification With Ghosts
Read the Docs
v: latest
Versions
latest
cvl1
Downloads
On Read the Docs
Project Home
Builds