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
Advanced Subjects
Method declarations
Summarizing Solidity Functions
Internal Function Summaries
More Expressive Summaries
Multicontract
Linking Contracts
Approximation
Advanced Debugging
Grounding
Best Practices
Common Pitfalls
Assert splitting
Troubleshooting
Certora Prover Documentation
»
Old Documentation
»
Advanced Subjects
Edit on GitHub
Advanced Subjects
Method declarations
Summarizing Solidity Functions
Calls inside the code
Internal Function Summaries
Allowed Summaries
Example
More Expressive Summaries
Ghost Summaries
CVL Function Summaries
Multicontract
Linking Contracts
Approximation
The Problem
Solution 1: Overapproximation
Uninterpreted Function as an Overapproximation
Axiomatized Uninterpreted Function as an Overapproximation
Advanced Debugging
Memory Analysis
Grounding
Flag
Grounding General Idea
Limitations
Alternating Quantifiers
Recursion
Variables That Are Not Arguments
Double Polarity
Simple Parameters
Read the Docs
v: latest
Versions
latest
cvl1
Downloads
On Read the Docs
Project Home
Builds