Certora

• Name: Certora
• URL: https://www.certora.com/
• Category: formal verification / smart-contract security / audit tooling
• Summary: Certora is one of the cleanest formal-verification anchors in the corpus. The real product is the prover-and-spec workflow, not generic audit services with a solver bolted onto the slide deck.
• What it does:
  • Provides the Certora Prover, which checks smart-contract code against specifications written in Certora Verification Language
  • Supports verification workflows across multiple ecosystems, including EVM, Solana, Soroban, Stellar, and Sui-related tooling
  • Publishes tutorials, examples, and mutation-testing or equivalence-checking tools that help teams write and harden specs
  • Offers formal-verification and audit services alongside the software stack
• Key claims:
  • The homepage says Certora secures smart contracts with formal-verification tools and audits, and markets the platform as protecting over $100B TVL
  • The official docs position the Certora Prover as the core product and list adjacent tools including the Certora Solana Prover, Sunbeam, Gambit, and the Equivalence Checker
  • The technical white paper says the prover translates low-level code plus CVL/CVLR specifications into mathematical formulas and uses solvers to find counterexamples or prove properties hold
  • Certora’s public GitHub organization highlights examples, tutorials, and a verification-and-audit portfolio, which makes the tooling surface visible
• Whitepaper: Certora does have an official technical white paper, published on its own site as a web document rather than a classic protocol PDF; see ../whitepapers/certora-primary-sources-2026-04-25.md.

Internal linkages

• Best comparisons: runtime-verification, trail-of-bits, and chainsecurity.

• Sources:

  • https://www.certora.com/
  • https://docs.certora.com/en/latest/
  • https://docs.certora.com/en/latest/docs/whitepaper/index.html
  • https://github.com/Certora

• Last reviewed: 2026-05-28 UTC