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