Formal verification is the only technique that can prove entire classes of bugs can't happen. However, for most developers, it has remained out of reach because it requires specialized expertise and significant manual effort.

For the past seven years, Certora has helped secure some of the most critical protocols in DeFi through manual audits and formal verification. Today, we're bringing that experience into AutoProver: a system that reads your code and documentation, generates formal specifications and tests, and formally verifies your software using state-of-the-art formal methods.

The result is more secure, easier-to-maintain code, with formal verification now accessible to every developer.

AutoProver Beta is available today for Solidity, with Rust coming soon. It integrates with existing LLMs, making it easy to incorporate into development workflows.

The problem: shipping speed has outrun shipping confidence

Today development is faster than ever, but confidence hasn't kept up. Three things are getting in the way.

• Logic bugs are hard to catch. The trickiest errors are logical, not syntactic. They compile, pass tests, and often survive code review. Then, weeks or months later, the right sequence of transactions exposes them. Manual code review catches some of these bugs, but it is slow, expensive, and doesn't scale.
• AI-generated code lacks guarantees. Models improve constantly, but they produce non-deterministic results and have no precise notion of intent. AI can generate working code remarkably well, but it has no understanding of whether that behavior matches your intent. It can also introduce subtle regressions that look perfectly reasonable during review.
• Formal verification doesn't scale. Formal verification is hard because writing good specifications takes experience. Most teams don't have formal methods experts sitting next to every developer.

The solution: an agentic pipeline from intent to proof

AutoProver brings together specialized AI agents built on years of formal verification research and engineering. The workflow is straightforward:

1. Understand your code

You point AutoProver at your repository, and it gets to work. It starts with the code you already have, using documentation and design docs to build a richer understanding of your system.

2. Generate formal specifications

It turns that understanding into formal properties covering both individual components and interactions across the system. These specifications describe the intended behavior, independent of the current implementation.

3. Generate tests and proofs

From those properties, AutoProver generates tests (currently in Foundry), CVL rules for the Certora Prover, and the supporting verification code needed to prove correctness.

4. Execute and investigate

Specialized agents run the generated tests and proofs, triage failures, and troubleshoot verification issues. Another agent looks for bugs that weren't explicitly specified, drawing on common vulnerability patterns learned from years of Certora verification work.

5. Review results. You receive a structured report in three parts: code bugs, design bugs, and the full status of every property, with its tests, rules, and results.

6. Iterate. Review the findings, give feedback, and rerun. AutoProver learns from your input over time. When you're ready, you can open a PR with the generated verification assets and continue evolving your verification suite alongside your code.

More than pattern matching

Most AI code review tools flag potential issues based on pattern matching. AutoProver takes a fundamentally different approach: it generates formal specifications and mathematically proves properties about your code using state-of-the-art formal verification methods.

Unlike conversational AI tools, AutoProver generates verification assets that become part of your development workflow. The tests, specifications, and verification rules it produces can be reviewed, versioned, and maintained alongside your application, growing into a long-term verification suite.

"I've been working in formal methods for more than four decades, and writing specifications has always been the bottleneck," says Mooly Sagiv, co-founder of Certora. "LLMs are changing how software gets written, but they aren't solving the correctness problem. If anything, they're making it even more important. AI can now help with one of the hardest parts of formal verification, making it practical and accessible to many more developers."

As easy to run as a compiler

Running AutoProver should feel as natural as running a compiler or any other development tool. AI has changed how quickly we can write software. AutoProver is built to help us trust it just as quickly.

Get started today

AutoProver Beta is available now for Solidity, with Rust coming soon.

Start now: https://app.certora.com/