Certora Prover Documentation
latest

Contents

  • Certora Technology White Paper
  • Certora User’s Guide
  • The Certora Verification Language
  • The Certora Prover
  • Gambit: Mutation Generator for Solidity
  • Equivalence Checking Using the Certora Prover
  • Old Documentation
    • Specification By Example
      • The Bank
      • The (Iterable) Map
    • The Anatomy of a Specification
    • Advanced Subjects
    • Best Practices
    • Common Pitfalls
    • Assert splitting
    • Troubleshooting
Certora Prover Documentation
  • »
  • Old Documentation »
  • Specification By Example
  • Edit on GitHub

Specification By Example

  • The Bank
    • Rules in the Certora Verification Language
    • Parametric rules
    • Invariants
      • Declaring functions used in the invariant
      • envfree functions
    • Understanding the results of the Certora Prover
  • The (Iterable) Map
    • Overview
    • A Simple Map
      • The code
      • Writing specs
        • Generalized unit tests
        • Revert conditions
        • Inverses
    • The IterableMap Contract
      • Adding iteration
      • A soft introduction to ghosts
    • Verification With Ghosts
Previous Next

© Copyright 2022, Certora, Inc. Revision 19a6cd2f.

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