Certora Prover Documentation Logo

Contents

  • Certora User’s Guide
    • Tutorial and Workshops
    • Installation
    • CI Configuration
    • Running the Certora Prover
    • Designing Good Specifications
    • Producing Positive Examples
    • Invariants
    • Parametric rules
    • Tracking changes with ghosts and hooks
    • Specification Design Patterns
      • Tracking Sums
      • Partially Parametric Rules
      • Listing Safe Assumptions
      • Require Invariants: Proving inter-dependent invariants
    • Using Opcode Hooks
    • Working with Multiple Contracts
    • Managing Timeouts and Out of Memory Problems
    • Understanding gaps between high and low level code
    • Checking Specifications
    • Glossary
  • The Certora Verification Language
  • The Certora Prover
  • Sunbeam: Verification for Soroban
  • Gambit: Mutation Generator for Solidity

Additional information

  • The Certora Equivalence Checker
  • Certora Technology White Paper
  • Index
Certora Prover Documentation
  • Certora User’s Guide
  • Specification Design Patterns
  • View page source

Specification Design Patterns

Certain patterns often occur in specification files. This chapter describes some of these patterns.

  • Tracking Sums
    • Enforcing Sum of Two Balances Constraint
    • Maintaining Equality Between Sum of Balances and Total Supply
  • Partially Parametric Rules
  • Listing Safe Assumptions
    • Context:
    • Importance of Listing Safe Assumptions:
  • Require Invariants: Proving inter-dependent invariants
    • Importance of Require Invariants:
Previous Next

© Copyright 2024, Certora, Inc.

Built with Sphinx using a theme provided by Read the Docs.