Certora Prover Documentation Logo

Contents

  • Certora User’s Guide
  • The Certora Verification Language
  • The Certora Prover
    • Introduction
    • Installation
    • Prover Approximations
    • Techniques Used by the Certora Prover
    • Diagnostic Tools
    • Checking Specifications
    • Certora Prover CLI
    • Using the Certora Portal
      • Certora Verification Reports
      • Special Portal URLs
    • Changelog
  • Sunbeam: Verification for Soroban
  • Gambit: Mutation Generator for Solidity

Additional information

  • The Certora Equivalence Checker
  • Certora Technology White Paper
  • Index
Certora Prover Documentation
  • The Certora Prover
  • Using the Certora Portal
  • View page source

Using the Certora Portal

  • Certora Verification Reports
    • Storage in Call Trace
      • Introduction
        • Example Storage Data
      • How Can the Storage Change?
      • When Do We Show the Storage State?
      • What Do We Show?
      • Computational Types
      • Limitations of the Current “Computational Type” Resolution
      • Reverts
      • Havocs
      • Call Resolution
    • Understanding counter-examples
  • Special Portal URLs
    • Job status
    • Additional error reports
    • Timeout analysis
    • Zip output
Previous Next

© Copyright 2025, Certora, Inc.

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