Certora

Certora develops software and services for verifying the correctness and security of smart contracts. Its core product is the Certora Prover, which takes low-level contract bytecode — EVM bytecode, a Solana eBPF object, or a Stellar WASM object — together with a specification written in the Certora Verification Language (CVL) or its Rust variant CVLR, and analyzes the two together to find executions in which the code deviates from the specification. The company describes the Prover as effectively a compiler that translates contract bytecode and specified properties into a mathematical formula, which is then passed to open-source solvers; violating scenarios are reported back as concrete call traces, while an unsolvable formula indicates the property cannot be violated. Certora contrasts this with testing and fuzzing, citing path explosion and state explosion as limits of test-based approaches, and with manual auditing, arguing that specifications can be re-checked automatically on every code change ("specify once, verify often").

Beyond the Prover, Certora's tool suite includes Gambit for assessing specification quality via mutations and vacuity detection, Safeguard for monitoring invariants within an Ethereum node, and Quorum for detecting errors in governance proposal payloads. In 2026 the company introduced AutoProver, described as combining AI agents with formal methods to infer intent from code, generate specifications automatically, and prove the absence of bugs. Alongside tooling, Certora sells security audits performed by dedicated auditors and formal verification experts, and runs community audit contests with platforms such as Code4rena to crowdsource custom formal specifications.

The company's website states that over $100B in total value locked has been protected using its tools. Named users and endorsers include Aave, Compound and Balancer, and published engagements cover Solana's P-Token program, the Suilend lending protocol on Sui, and 1inch's cross-chain swap mechanism.

Business model

Certora combines a self-serve software product with expert services. The Certora Prover is offered in a free Basic tier (up to 2,000 minutes per month of runtime, self-written rules, Discord support), a Premium tier (unlimited Prover access, onboarding support, up to 10 team members, specification review), and an Enterprise tier described as an audit plus formal verification retainer in which Certora experts write rules for customer code, with unlimited Prover access, training, dedicated support and incident response. Premium and Enterprise pricing is not published and is handled through sales contact. Separately, Certora sells smart contract security audits delivered by a dedicated team producing a detailed report through an interactive process.

Subscription/tiered access to the Certora Prover (free Basic tier, paid Premium and Enterprise tiers, the latter structured as an audit and formal verification retainer) plus fee-based security audit engagements. Certora has also received grants, including from the Canton Development Fund and the Ethereum Foundation.

Traction

Certora's site claims over $100B in total value locked protected. Executives at Aave, Compound and Balancer are quoted describing use of the Prover, with Aave noting vulnerabilities found that are usually hard to detect in manual review. Published 2026 work includes verifying Solana's P-Token as a drop-in replacement for SPL Token, formal verification of the Suilend lending protocol, a security review of 1inch cross-chain swaps, and a security framework for Aave V4. A year-in-review post states the security research team quadrupled in size during 2025. A funding report lists 125 employees as of March 2026.

Latest developments

In July 2026 Certora introduced AutoProver, an agentic formal verification product; an August 2026 post compared AutoProver's independently generated specification for the Aave v4 Hub against a human-authored verification engagement, reporting that AutoProver proved substantial solvency and accounting properties while also showing the need for expert analysis of protocol intent and economic safety. Other recent items include a July 2026 post on formal verification of a Solana staking protocol, a Canton Development Fund grant to build an open-source static analysis tool for Daml contracts (May 2026), and the $36.0M raise reported in March 2026.