Certora Prover Documentation
latest
Contents
Certora Technology White Paper
Certora User’s Guide
Introduction
Tutorial and Workshops
Getting Started
Specification By Example
Designing Good Specifications
Specification Design Patterns
Working with Multiple Contracts
Managing Timeouts
Checking specifications
Troubleshooting
Frequently Asked Questions
Glossary
The Certora Verification Language
The Certora Prover
Gambit: Mutation Generator for Solidity
Old Documentation
Certora Prover Documentation
»
Certora User’s Guide
Edit on GitHub
Certora User’s Guide
Introduction
Tutorial and Workshops
Tutorial
Stanford DeFi Security Summit
EthCC Paris
Aave Community Day
Getting Started
Installation
Project Layout
Running the Certora Prover
Specification By Example
Designing Good Specifications
Method Specifications
Variable Changes
Variable Relationships
State-Transition Systems
Risk Assessment
Mathematical Properties
Specification Design Patterns
Tracking Sums
Partially Parametric Rules
Listing Safe Assumptions
Writing State-Based Invariants
General Rules
Working with Multiple Contracts
Example protocol
Handling unresolved method calls
Working with known contracts
Working with unknown contracts
Conclusion
Managing Timeouts
What causes timeouts?
The complexity check
Summarizing complex functions
Flags for tuning the Prover
Checking specifications
Troubleshooting
Frequently Asked Questions
Glossary
Read the Docs
v: latest
Versions
latest
Downloads
On Read the Docs
Project Home
Builds