Certora Verification Reports

• Storage in Call Trace
  • How can the storage change?
  • When do we show the storage state?
  • What do we show?
  • What are the “computational types”?
  • Limitations of the current “computational type” resolution

Todo

This documentation is incomplete. See Understanding the results of the Certora Prover in the User’s Guide.