Certora Prover Documentation
74
Contents
Certora Technology White Paper
Certora User’s Guide
Introduction
Tutorial and Workshops
Getting Started
Specification By Example
Designing Good Specifications
Producing Positive Examples
Specification Design Patterns
Tracking Sums
Partially Parametric Rules
Listing Safe Assumptions
Writing State-Based Invariants
General Rules
Solvency Rules
Valid States and Transitions
Rules for ERC20
Working with Multiple Contracts
Managing Timeouts
Checking specifications
Troubleshooting
Frequently Asked Questions
Glossary
Contacting Certora
The Certora Verification Language
The Certora Prover
Gambit: Mutation Generator for Solidity
Equivalence Checking Using the Certora Prover
Old Documentation
Certora Prover Documentation
»
Certora User’s Guide
»
Specification Design Patterns
»
General Rules
Edit on GitHub
Warning
This page
was created
from a pull request (
#74
).
General Rules
Todo
This section is incomplete.
Solvency Rules
Valid States and Transitions
Rules for ERC20
Read the Docs
v: 74
Versions
latest
cvl1
Downloads
On Read the Docs
Project Home
Builds