Certora Prover Documentation
Contents
Certora User’s Guide
The Certora Verification Language
The Certora Prover
Introduction
Installation
Prover Approximations
Techniques Used by the Certora Prover
Diagnostic Tools
Checking Specifications
Certora Prover CLI
Using the Certora Portal
Certora Verification Reports
Special Portal URLs
Changelog
Sunbeam: Verification for Soroban
Gambit: Mutation Generator for Solidity
Additional information
The Certora Equivalence Checker
Certora Technology White Paper
Index
Certora Prover Documentation
The Certora Prover
Using the Certora Portal
View page source
Using the Certora Portal
Certora Verification Reports
Storage in Call Trace
Introduction
Example Storage Data
How Can the Storage Change?
When Do We Show the Storage State?
What Do We Show?
Computational Types
Limitations of the Current “Computational Type” Resolution
Reverts
Havocs
Call Resolution
Understanding counter-examples
Special Portal URLs
Job status
Additional error reports
Timeout analysis
Zip output