Certora

Certora is a smart contract security company whose core conviction is captured in its tagline: "Move fast, break nothing." The company builds formal verification tools that apply mathematical proof techniques to smart contract code, enabling developers and auditors to detect vulnerabilities with a degree of rigor that conventional testing and manual code review cannot match.

What Formal Verification Does

Traditional smart contract security relies on testing — which can only cover scenarios a developer thinks to write — and manual review, which depends on human attention and expertise. Formal verification takes a different approach: it converts a contract's logic into mathematical formulas and uses automated solvers to check every possible state and execution path. If a vulnerability exists, the prover finds a counterexample. If none exists, it produces a proof of correctness.

Certora's flagship tool, the Certora Prover, implements this approach. Developers write specifications in the Certora Verification Language (CVL), a domain-specific language for expressing properties the contract must satisfy. The Prover checks those properties against the contract's compiled bytecode rather than its source code, meaning the analysis reflects what actually executes on-chain rather than what a developer intended to write.

Open-Source Prover

In February 2025, Certora made the Prover open source under the GNU General Public License v3. The company framed this as a democratization move: formal verification had previously been expensive enough that only well-funded protocols could access it, while smaller projects relied on cheaper and less rigorous methods. By open-sourcing the engine, any development team can now integrate formal verification directly into their build pipeline at no cost.

The open-source Prover covers EVM-compatible chains, Solana (via Solana Binary Format, sBPF), and Stellar (via WebAssembly). Documentation and example specifications are publicly available, and the tool can be run locally or through Certora's cloud interface.

AutoProver: AI-Assisted Specification

Writing formal specifications has historically been the main barrier to adoption. Expressing contract invariants and properties in CVL requires expertise that most development teams lack. In July 2026, Certora launched AutoProver to address this.

AutoProver combines AI agents with formal methods to infer developer intent from existing code and documentation, then generates specifications automatically and proves them. A developer feeds it a codebase and any design documents written in plain English; AutoProver produces the formal specs and runs the proofs without requiring manual CVL authorship. A comparison published in August 2026 pitted AutoProver's AI-generated specifications against hand-written specs for Aave v4, testing the quality ceiling of the automated approach. The tool currently targets Solidity; Rust and Solana support are in development.

Solana Integration

Certora's Solana Prover analyzes Rust-based Solana smart contracts at the bytecode level. The tool compiles contracts to sBPF bytecode, decompiles that bytecode into an intermediate representation using abstract interpretation techniques, and generates logical formulas for SMT solvers to check. The bytecode-level approach verifies the code that actually executes on the Solana validator network rather than an abstracted source model.

Certora formally verified SPL Token 2022 and P-Token, a Solana SPL Token performance optimization, producing machine-checked proofs that the token programs behave correctly across all possible states. A July 2026 blog post described formal verification of what Certora called "Solana's most battle-tested staking protocol," applying the Solana Prover to a live staking program. At Breakpoint 2025, Certora highlighted a subsidized security program making up to 1 million USD available to Solana projects seeking formal verification coverage — an effort to accelerate adoption before most projects would invest in it independently.

Scale and Track Record

In 2025, Certora's tools and audit services helped secure 196.5 billion USD in total value locked and prevented more than 720 vulnerabilities from reaching production. Fourteen of the top twenty DeFi protocols by TVL engaged Certora during 2025, with seven of the top ten maintaining ongoing long-term engagements.

Clients include Aave, MakerDAO, Uniswap, Lido, Compound, Balancer, EigenLayer, the Ethereum Foundation, and the Solana Foundation. Certora's public GitHub repository contains security reports for verified protocols, providing transparency into what properties were proved and where issues were identified.

Services

Certora operates through three service lines. The core product is the Certora Prover, now open source, for teams that run verification themselves. For teams that want expert support, Security Audits pair formal verification specialists with traditional audit methodologies to produce detailed security reports through an interactive engagement process. Community Contests, run in partnership with platforms like Code4rena, crowdsource vulnerability discovery through security competitions, complementing the formal verification work with a broader pool of researchers.

Background

Certora was founded on the thesis that formal methods developed in academic and safety-critical software engineering could be made practical for the pace of Web3 development. The team has developed the Prover over more than seven years. Its trajectory — from a commercial service accessible only to the largest protocols, to an open-source tool with AI-assisted specification generation and multi-chain coverage — reflects a consistent push toward making proof-grade security broadly accessible.

With the open-source Prover now supporting Solana, an active subsidized security program, and AutoProver Rust support on the roadmap, Certora is one of the few security-focused projects bringing formal mathematical verification to the Solana development toolchain.