Warning

This page was created from a pull request (#74).

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