Certora

Certora is a formal verification company, founded in 2018 and headquartered in Tel Aviv per its own press boilerplate, that builds the Certora Prover and sells both formal verification and manual security audits. It fits DeFi teams whose core risk is in protocol invariants (solvency, accounting, governance) and who want machine-checked properties alongside a manual review. Its report index is active, with formal verification reports for Aave V4, Solana programs and Stellar contracts published between June and September 2026, and the Prover itself has been released under the GPL-3.0 licence.

At a glance

Founded	2018, per the firm's press release boilerplate (Chainwire release)
Headquarters / jurisdiction	Tel Aviv-Yafo, Israel (Chainwire release)
Engagement model	private firm audit and formal verification, Prover licensing, and an audit + FV retainer tier (pricing)
Core specialties	formal verification with the Certora Prover; manual security audits (homepage)
Ecosystems / languages	EVM (Solidity), Solana (Rust), Stellar (Soroban), Sui (Move) in manual audits (reports)
Public report index	certora.com/reports
Open-source tooling	Certora Prover (GPL-3.0), Gambit mutation tester, CVLR, AI Composer (Prover repo, GitHub)
Published pricing	Prover Basic tier is free up to 2,000 min/month; Premium and Enterprise (audit + FV retainer) are quote-only (pricing)

What they do

Certora's homepage describes three offerings: the Certora Prover, which checks contract code against written rules across all states and paths; security audits by a dedicated team with formal verification expertise; and community contests run with partners such as Code4rena (homepage). The pricing page lists a free Basic Prover tier, a Premium tier with unlimited Prover use and specification review, and an Enterprise tier described as an "audit + formal verification retainer" with expert rule-writing by Certora's team and incident response included (pricing).

In November 2025 the firm announced AI Composer, an open-source platform combining AI code generation with formal verification (Chainwire release). Audit requests go through a signup flow on the site (homepage).

Specialties and ecosystem coverage

The report index labels each item as Formal Verification, Manual Audit or both. EVM DeFi dominates: Aave (13 report links on the index page), Compound (9), Lido (7, including Lido V3 work from December 2025 and January 2026) and Balancer (7), counted from the page source on 2026-09-24 (reports). A Uniswap v4 report is published (Uniswap v4).

Non-EVM coverage is evidenced: Solana formal verification (Solana Stake Pool, Solana P-Token) (Solana Stake Pool, Solana P-Token); Stellar Soroban audit and FV for OpenZeppelin's Stellar Contracts library (OpenZeppelin Stellar); and a manual audit of Aftermath Finance's perpetuals exchange, built in Move on Sui (Aftermath).

Against the directory: Ethereum, Solana and Stellar are confirmed; Sui is evidenced but not listed. Polygon, Arbitrum and Optimism are not visible in report titles. Of the notable audits, Aave, Uniswap, Lido and Compound are confirmed; no report branded MakerDAO was found, though several Spark reports appear in the index (reports).

Recent public work

Pulled from the Certora report index, newest first:

• OpenZeppelin Stellar Contracts, audit and FV (Soroban), September 18, 2026: 44 findings (report)
• Aftermath Finance Perpetuals (Sui, Move), manual audit, August 24, 2026 (report)
• Royco Day, manual audit, August 18, 2026 (report)
• Aave Stable Vault, FV, August 13, 2026 (report)
• Solana Stake Pool, FV, July 16, 2026 (report)
• Aave V4 Hub (with Libraries, Spoke and Tokenization Spoke reports), FV, July 8, 2026 (report)
• Spectra Bridge (Stellar/Ethereum), manual audit, June 10, 2026 (report)
• Solana P-Token, FV, June 4, 2026 (report)
• Lido V3 audit, January 2026 (report)

Research, tooling and methodology

The Certora Prover's source is public on GitHub under GPL-3.0 and supports EVM, Solana and Stellar (Prover repo). The GitHub organization also hosts Gambit (a mutation tool for testing specs), CVLR (a verification language for Rust), a SecurityReports repository, tutorials and examples (GitHub). The FV reports describe the method as proving the implementation correct against formal rules written by Certora's team (Solana Stake Pool).

A buyer should understand the method's limit, which Certora itself spells out in its Balancer write-up: formal verification proves only the properties that are written, and properties that do not constrain a behavior cannot catch bugs in it (Certora on Balancer).

Track record and incidents

Balancer V2, November 3, 2025. Balancer V2 Stable Pools were exploited through a rounding-direction error. In its own post-mortem, Certora states that its 2022 review of Balancer v2 Stable Pools used the Prover and manual review to prove key solvency properties, and that those properties "were not strong enough to detect the rounding error" because they "did not constrain the relationship between individual swaps or rounding behavior" (Certora on Balancer). Certora says it helped investigate and, with Balancer, checked whether other v2 pool types were affected. Trail of Bits, another prior Balancer auditor, points readers to Certora's post for root-cause analysis and notes its own 2021 review had flagged similar rounding issues (Trail of Bits). On the scope question: Certora's review covered Balancer v2 Stable Pools, but its write-up does not state whether the exact exploited pool code and commit were in that scope, and rounding behavior was not among the properties it verified. Trail of Bits also reviewed Balancer v2, and an exploit after an audit is not by itself proof of a missed finding.

No other reputable post-audit incident naming Certora was found in this pass.

Who should consider them — and who might look elsewhere

The strongest public evidence is long-running formal verification of large EVM lending, staking and AMM protocols (Aave, Lido, Compound, Balancer), with growing Solana and Stellar work. It fits teams that can state clear invariants and want them machine-checked, and teams that want to keep running the open-source Prover in CI after the engagement. Teams that mainly need a fast manual review of a small contract, or that have no in-house capacity to maintain specs, may get less from the FV-heavy model; buyers should ask which properties will be verified and which risks, such as rounding, sit outside them.

How to engage

Start via the audit signup on the Certora homepage, or the pricing page for Prover plans and the Enterprise retainer. Prepare a spec of the invariants that matter most, a fixed commit, and a plan for who on your team will maintain the Prover rules afterward.

Gaps and unverified claims

• Founding year is 2018, from a firm-issued press release, matching the directory. The site's /about URL returned 404.
• Team size is not published; the directory's 50+ could not be confirmed.
• Audit pricing and turnaround are not published.
• "Over $100B TVL protected" on the homepage is self-reported.
• No report branded MakerDAO was found; Spark reports are present.
• The directory's report URL certora.com/audits is a featured-reports landing page; the full index is at certora.com/reports, which served 142 distinct report links on 2026-09-24 (counted from page source).

Sources

1. Certora homepage, accessed 2026-09-24
2. Certora pricing, accessed 2026-09-24
3. Certora report index, accessed 2026-09-24
4. Certora audits landing page, accessed 2026-09-24
5. Chainwire: Certora launches AI Composer, accessed 2026-09-24
6. Certora GitHub organization, accessed 2026-09-24
7. CertoraProver repository, accessed 2026-09-24
8. OpenZeppelin Stellar Contracts report, accessed 2026-09-24
9. Aftermath Finance Perpetuals report, accessed 2026-09-24
10. Royco Day report, accessed 2026-09-24
11. Aave Stable Vault FV report, accessed 2026-09-24
12. Solana Stake Pool FV report, accessed 2026-09-24
13. Aave V4 Hub FV report, accessed 2026-09-24
14. Spectra Bridge report, accessed 2026-09-24
15. Solana P-Token FV report, accessed 2026-09-24
16. Lido V3 audit report, accessed 2026-09-24
17. Uniswap v4 report, accessed 2026-09-24
18. Certora: Breaking down the Balancer hack, accessed 2026-09-24
19. Trail of Bits: Balancer hack analysis, accessed 2026-09-24