Certora

Certora is a smart contract security company that builds formal verification tools — mathematical techniques that prove code is correct across every possible state and input, not just the ones developers thought to test. Its core product, the Certora Prover, has been in development for over seven years, now operates across EVM chains, Solana, Stellar, and Sui, and has been used to secure more than $100 billion in total value locked across the most prominent DeFi protocols in the industry. In February 2025 the company open-sourced the Prover, bringing industrial-grade verification to the broader developer community.

Core Mechanism

Traditional smart contract security relies on audits and tests: humans reading code for mistakes, and automated suites checking specific scenarios. Both approaches share a fundamental limit — they can only catch bugs in the cases they examine. Formal verification sidesteps that limit by using mathematical proofs.

The Certora Prover works at the bytecode level. When a developer submits a contract for verification, the Prover does not read the Solidity or Rust source; it analyzes the compiled bytecode that actually executes on-chain. This matters because compiler bugs can silently alter a program's behavior between the code a developer writes and the code that runs. By targeting bytecode, Certora verifies what is actually deployed.

Developers write specifications in one of Certora's domain-specific languages — CVL (Certora Verification Language) for EVM chains, and CVLR for Solana's Rust-based programs. These specs express properties the contract should always satisfy: "the total supply can never exceed the mint cap," or "a user's balance after a withdrawal must equal their previous balance minus the amount withdrawn." The Prover then uses Satisfiability Modulo Theories (SMT), a class of formal logic solvers, to check these properties against all possible inputs simultaneously. A run either returns a mathematical proof that the property holds, or produces a concrete counterexample showing exactly how it can be violated.

The practical effect is exhaustive coverage. Testing a withdrawal function might cover a handful of input values. The Certora Prover covers every value that could ever be passed. Subtle reentrancy conditions, overflow edge cases, and state-machine violations that live at the margins of input space — the places conventional testing almost never reaches — become visible.

Solana Integration

Certora added Solana support through the Solana Certora Prover (SCP), which targets Solana's sBPF (Solana Berkeley Packet Filter) bytecode. The pipeline works in stages: Rust programs compile to SBF bytecode, a custom decompiler lifts that bytecode into Certora's internal representation using abstract-interpretation-based analyses (including stack scalarization and alias analysis), and then the lifted code converts to logical formulas that the SMT engine solves.

A significant example of the Solana Prover in production is the verification of P-Token, a reimplementation of Solana's SPL Token program built on the Pinocchio framework. P-Token claims to cut compute unit consumption by approximately 95% versus the original SPL Token. Certora verified three equivalence properties between the two programs: that neither panics, that P-Token succeeds identically to SPL Token when SPL Token succeeds (with byte-for-byte matching account states), and that P-Token fails consistently with SPL Token when errors occur. This kind of equivalence verification — mathematically confirming that a performance-optimized rewrite preserves the semantics of the original — is a use case particularly well suited to formal methods.

Other Solana ecosystem clients include the Solana Foundation itself, Kamino Lending, Squads (a multisig protocol), Jito (liquid staking and MEV infrastructure), and Manifest. Certora also participates in the Solana Foundation Delegation Program.

Product Suite

Certora Prover remains the flagship product. As of February 2025 it is open source, available on GitHub under the Certora organization. The open-source release covers EVM, Solana (sBPF), and Stellar (WASM) verification.

Gambit is a mutation testing tool that helps developers stress-test their specifications. It systematically introduces small changes — mutations — to contract code, then checks whether the formal specs catch the resulting bugs. If a mutation goes undetected, the spec is incomplete.

Certora AI Composer, launched November 2025, is described as the first AI coding platform purpose-built for smart contracts with safety guarantees. Rather than generating code and hoping it is correct, it integrates with the Prover to verify that AI-generated code satisfies user-specified properties before it ships.

Safeguard, released February 2025, is a Geth extension for runtime monitoring. It continuously checks Ethereum protocol invariants in production rather than relying solely on pre-deployment verification — catching unexpected behavior if real-world conditions diverge from what was formally proved.

Quorum, released January 2025, applies formal verification techniques to DAO governance, automating detection of governance attack vectors and parameter configurations that could harm protocol safety.

Clients and Track Record

The company's client list spans much of blue-chip DeFi: Aave, MakerDAO, Uniswap, Lido, EigenLayer, Compound, Balancer, Morpho, Ether.fi, Safe, and Silo on the EVM side. Infrastructure organizations including the Ethereum Foundation and Coinbase have also worked with Certora. The Prover has operated in continuous integration pipelines for many of these projects, running verification checks on every code commit rather than solely at audit milestones.

In aggregate the company claims to protect more than $100 billion in total value locked — a figure that reflects the combined TVL of all protocols where Certora has performed verification work.

Team and Funding

Certora was founded in November 2018 by Mooly Sagiv (CEO) and Shelly Grossman (CTO). Sagiv is a computer science professor whose academic research in static analysis and program verification directly informs the Prover's architecture. The company employs between 50 and 200 people and is headquartered in Israel, with a presence in the United States.

Certora has raised $43.2 million across two funding rounds. A Series B round in May 2022 raised $36 million and was led by Jump Crypto, with participation from a broad group of investors. Jump's investment thesis emphasized Certora's role in enabling safe, rapid protocol development — the idea that formal verification removes the audit bottleneck that otherwise slows engineering teams.

No Token

Certora does not have a native token. The company operates as a commercial software and services business. Access to the Certora Prover requires an API key; the open-source release provides the core engine, but the cloud verification service remains a commercial offering.

Relevance to Solana

Certora's investment in Solana verification infrastructure is substantive. The Solana Prover targets sBPF bytecode directly, which means it covers Rust programs whether written with Anchor, native Solana, or Pinocchio. The company has published detailed technical analysis of core Solana programs including SPL Token extensions, and its blog consistently covers Solana security topics. For a Solana developer building a protocol with meaningful TVL — lending, liquid staking, AMMs — Certora represents one of the most rigorous security tools available, alongside traditional audits. The open-source release of the Prover in 2025 also means independent researchers and smaller teams can run verification locally before engaging Certora's professional services.