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
Previous Next

© Copyright 2022, Certora, Inc. Revision 1076df8a.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
Downloads
On Read the Docs
Project Home
Builds