Certora

• Name: Certora
• URL: https://www.certora.com/
• Category: formal-verification company / smart-contract assurance workflow operator / specification-language steward
• Tags: ethereum-ecosystem solana-ecosystem
• Summary: Certora belongs in companies/, not only projects/, because the useful question is not just what prover exists? but which named operator stewards the specification language, chooses the supported runtime and solver surface, packages verification engagements, and turns formal properties into workflow truth teams may start treating as release-gating authority? The practical leverage sits less in one proof run than in who defines the spec idioms, toolchain assumptions, example corpus, and managed-review posture that other teams inherit when they route security work through Certora.
• What it does:
  • Maintains the Certora Prover and Certora Verification Language workflow that let teams write properties over smart-contract systems and check implementations against those properties
  • Stewards adjacent tooling including the Certora Solana Prover, Sunbeam, Gambit, and the Equivalence Checker, which broadens the company boundary beyond one solver invocation
  • Packages verification and audit services around that tooling so the company can become part of a customer’s real review and release workflow rather than staying a passive software vendor
  • Publishes examples, tutorials, and public portfolio material that shape how downstream teams learn to express and reason about smart-contract invariants
  • Extends the stack across multiple ecosystems, including EVM, Solana, Soroban, Stellar, and Sui-related tooling, which makes Certora’s support and prioritization choices matter beyond a single chain family
• Key claims:
  • The homepage frames Certora as securing smart contracts with formal verification tools and audits, which is useful because the company is presenting itself as a workflow authority rather than a narrow research artifact
  • The docs position the Certora Prover as the core product and list adjacent tools including the Certora Solana Prover, Sunbeam, Gambit, and the Equivalence Checker, confirming that the company boundary spans a broader verification stack
  • The technical white paper says the prover translates low-level code plus CVL or CVLR specifications into mathematical formulas and uses solvers to find counterexamples or prove properties hold, which makes the language and prover assumptions a meaningful control surface
  • The public GitHub organization highlights examples, tutorials, and a verification-and-audit portfolio, reinforcing that Certora steers not only the software but also the public demonstration layer for what good formal-spec work looks like
• Whitepaper: Certora does have an official technical white paper, published on its own docs site as a web document rather than a classic protocol PDF; see ../whitepapers/certora-primary-sources-2026-04-25.md.
• 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

Internal linkages

• Keep the project / company split explicit: certora is the reusable prover-and-specification stack, while this note is the entity boundary around language stewardship, support coverage, managed verification workflow, and release-gating influence.
• Useful adjacent company reads: chainsecurity, trail-of-bits, and informal-systems.
• Useful adjacent company read when the question broadens from Certora’s prover stack to a more semantics-heavy formal-methods operator: runtime-verification.

Protocol / company boundary

• The project layer still matters because the prover, CVL, examples, and related tools are reusable engineering surfaces in their own right.
• The company layer matters separately because Certora decides how the language evolves, which runtimes and patterns get first-class support, how example properties are taught, and how formal verification is packaged into customer review and release workflow.
• That is why this note belongs in companies/: the sharper questions are about who authors the formal-spec defaults and managed verification posture, not only about one prover binary.

Control surface

• Practical leverage sits in the semantics and ergonomics of CVL, the supported backend and ecosystem matrix, the assumptions exposed or hidden by tooling defaults, and the public examples or templates teams copy into their own verification programs.

• The sticky dependency is workflow authority: once a protocol treats Certora-authored properties, proof outputs, or managed review cadence as part of its deploy-or-don’t-deploy decision process, the company becomes part of the effective release boundary even without holding onchain keys.

• Read Certora as a formal-verification company and assurance-workflow steward first, not just as a neutral prover artifact.

• Last reviewed: 2026-08-07 UTC