Certora is extending AutoProver, our agentic formal verification tool, to Rust and building native support for Solana programs. The goal is to make formal verification something developers can run throughout a build rather than commission through a dedicated engagement.

For a Solana program that governs user funds, critical assumptions need to hold from the moment it goes live. Once a lending market or perps exchange is operating, a broken invariant can put funds at risk before a team has time to respond.

Testing catches the cases developers think to write. Formal verification goes further by mathematically checking whether a defined property holds across every execution admitted by the program model. Historically, that level of assurance has required specialist verification engineers and hand-written specifications. AutoProver automates much of that work, bringing prover-backed analysis into the regular development process.

How AutoProver Works

Developers give AutoProver their code and, when available, additional context such as design documents or threat models. AutoProver analyzes the implementation, generates candidate formal properties, specifications, and tests, runs verification, and investigates the failures it finds. Additional context helps guide the analysis, but it is not required.

AI analyzes the code, proposes candidate properties, and helps interpret the results. Certora’s prover then checks those properties against the program model. It attempts to prove that each property holds and can produce a counterexample when a property is violated.

This combination keeps proof as the final arbiter. AI helps scale the specification and analysis process, while the prover supplies mathematical assurance for each property it successfully verifies.

Developers review the generated properties, add context, inspect findings, and iterate as the implementation changes. The output is a report covering issues found, properties verified, and the tests and verification rules produced during the analysis. Those artifacts can be refined and committed alongside the codebase, turning verification into part of the development process rather than a one-time exercise.

Built on Existing Work Across Solana

Certora began developing formal verification technology for Solana back in 2023. Since then, we have worked with Kamino, Squads, Manifest, and Jito to formally verify Solana programs and formally verified SPL Token-2022 for the Solana Foundation.

Each of those engagements paired Certora verification engineers directly with a protocol team. That model provides strong assurance for high-value programs, but its reach is limited by the number of specialist engineers available to support individual engagements. AutoProver extends the reach of the same underlying verification technology, making it accessible to developers without requiring a bespoke engineering engagement for every verification run.

“Formal verification has always been able to prove that critical properties hold. What it hasn’t been able to do is scale to every team that needs it,” said Mooly Sagiv, Founder of Certora. “AI agents can help solve that scaling problem, but they cannot replace proof. An agent can read code and suggest what should be true, but a suggestion is still just a suggestion. AutoProver pairs those agents with a proof engine, so AI helps scale the process while the prover still has to establish whether each property actually holds. Extending that approach to Rust and Solana is a natural next step.”

What Comes Next

AutoProver launched for Solidity in July 2026. Work on the Rust extension and native Solana verification pipeline is now underway, with an initial Solana version targeted for around Solana Breakpoint in November 2026.

The goal is for teams to check their critical assumptions continuously as the code changes, before those assumptions surface as findings during an audit or failures in production.

This work is open source and already underway. Developers can explore the code and follow its development on GitHub:

• Lusterna — our open source tool for reasoning about Rust programs with Lean 4: https://github.com/Certora/lusterna
• AutoProver — Certora’s agentic formal verification platform: https://github.com/Certora/autoprover

Work With Certora

Certora helps protocols, infrastructure providers, and financial institutions strengthen software security through expert security reviews, AI-powered analysis, and formal verification. To learn more about AutoProver visit app.certora.com.