Breakpoint 2025: Security Block: Certora (Pamina Georgiev)

When millions of dollars in cryptocurrency are at stake, "probably secure" isn't good enough. At Breakpoint 2025, Pamina Georgiev, Formal Verification Team Lead at Certora, demonstrated how mathematical proofs can guarantee that smart contracts behave exactly as intended—eliminating the element of chance from security testing entirely.

Summary

Formal verification represents a paradigm shift in how DeFi protocols approach security. While traditional testing methods like unit tests and fuzz testing can find bugs through random sampling, they can never guarantee the absence of vulnerabilities. Certora's approach uses mathematical specification and automated theorem proving to exhaustively verify that code behaves correctly under all possible conditions.

Georgiev walked the audience through a practical example using a simple vault contract—the kind of code that handles deposits and withdrawals in countless DeFi applications. She intentionally introduced a rounding bug that would cause the protocol to overpay users by approximately one token per withdrawal. Despite running 100,000 fuzz tests, the bug went undetected. However, Certora's formal verification tool caught the vulnerability in roughly 30 seconds, providing a specific counterexample that demonstrated exactly how the exploit worked.

The company has already established itself as a trusted security partner for major Solana projects, having completed formal verification work for Jito, Kamino, Squads, and Manifest, as well as direct work with the Solana Foundation. Beyond formal verification, Certora offers comprehensive security services including audits, design reviews, and operational security support.

Key Points:

The Limitations of Traditional Security Testing

Most DeFi protocols employ a multi-layered security approach that includes internal and external code reviews, auditing, unit testing, and fuzz testing. While fuzz testing represents an improvement over simple unit tests by covering a broader range of inputs, it still fundamentally relies on luck. Finding bugs through random sampling is essentially "a game of chance"—sometimes you discover vulnerabilities, and sometimes they slip through undetected.

Georgiev emphasized that when real money is at stake, this probabilistic approach creates unacceptable risk. If users' funds can be exploited, trust in the protocol is permanently damaged. Formal verification addresses this limitation by providing mathematical guarantees rather than statistical confidence. Instead of testing a sample of possible inputs, formal verification proves that properties hold for all possible inputs and all reachable states of the program.

How Formal Verification Works

Formal verification involves writing mathematical specifications that describe the intended behavior of code, then using automated theorem provers to derive those properties from the actual implementation. Certora has developed a specialized verification language for Rust that allows developers to write specifications that resemble familiar test code.

The process requires developers to think carefully about what properties their code should satisfy. In the vault example, an important property is that the share value (total assets divided by total shares) should never decrease after any user operation. If this property is violated, it means the protocol is overpaying users, which will eventually result in insufficient funds for later withdrawals.

When running verification, the tool considers all possible inputs (represented as non-deterministic values) and all possible starting states that the program could legitimately reach. If any combination violates the specified property, the prover produces a counterexample—a concrete scenario demonstrating the failure.

Certora's Solana Prover in Action

Certora's Solana prover is open source and comes with a command-line tool that makes verification accessible to developers. The prover sends verification tasks to the cloud and returns results through a web interface that includes detailed counterexamples when properties fail.

In the demonstration, the prover identified the rounding bug by finding a specific scenario: starting with 19 assets and 10 shares, when a user redeems 6 shares, they receive 12 assets instead of their fair share of 11. This concrete counterexample made the bug immediately apparent and pointed directly to the fix—changing the rounding direction in the division operation.

The verification process took approximately 30 seconds, including network latency. Once the fix was applied, the prover confirmed that the property now held for all possible inputs and states.

Security Subsidies for Solana Builders

Georgiev announced an important funding opportunity through Anza's security subsidy program, which provides up to one million dollars for Solana builders to access security services. Certora is a participating vendor in this program, meaning developers can potentially receive subsidized access to both auditing and formal verification services.

This initiative reflects the broader ecosystem's commitment to security and provides a practical path for projects of all sizes to access enterprise-grade security tools and expertise.

Facts + Figures

• Certora has completed formal verification projects for Jito, Kamino, Squads, Manifest, and the Solana Foundation
• Fuzz testing with 100,000 passing cases did not detect a rounding vulnerability that formal verification found in approximately 30 seconds
• The rounding bug in the example vault caused overpayment of approximately 1 token per withdrawal
• The specific counterexample found: 19 assets, 10 shares, user redeems 6 shares and receives 12 assets instead of the correct 11
• Anza's security subsidy program provides up to $1 million in funding for Solana builders to access security services
• Certora's Solana prover is open source and available via command-line tool
• Certora offers comprehensive security services including audits, design reviews, operational security, and formal verification

Top quotes

• "Formal verification is basically the only way to guarantee any of that."
• "Still to find bugs with fuzz testing, it's a little bit a game of chance. Sometimes you're lucky and you find the bugs, sometimes you're just not."
• "If you're handling money, you cannot get wrecked. Otherwise the trust is gone."
• "Even with 100K passing cases, it does not necessarily mean that you're bug free."
• "The only way to actually guarantee it is to formally verify."
• "A counter example means we have one specific, one concrete state of values where our property is violated."

Questions Answered

What is formal verification and how does it differ from regular testing?

Formal verification is a mathematical approach to proving that code behaves correctly under all possible conditions. Unlike traditional testing, which checks code against a finite set of inputs and scenarios, formal verification mathematically specifies the intended behavior and then proves that the code satisfies those specifications for every possible input and reachable state. This eliminates the element of chance present in fuzz testing, where bugs might go undetected simply because the random sampling didn't happen to trigger them. Formal verification provides mathematical guarantees rather than statistical confidence.

Why is formal verification particularly important for DeFi applications?

DeFi applications handle real money, making security failures catastrophic for user trust. When a vulnerability is exploited and funds are lost, the damage to a protocol's reputation is often irreparable. Traditional testing methods can reduce risk but cannot eliminate it—there's always a chance that a bug exists in an untested edge case. Formal verification is the only method that can provide guarantees about code behavior, which is essential when the stakes involve potentially millions of dollars in user assets. Even subtle bugs like incorrect rounding can drain a protocol over time.

How long does formal verification take compared to finding bugs manually?

In the demonstration at Breakpoint, Certora's prover identified a rounding vulnerability in approximately 30 seconds, including the time to send the verification task to the cloud and receive results. The same bug went undetected through 100,000 fuzz tests. Once a specification is written, the verification process is highly automated and can exhaustively check properties that would be impractical to test manually. The upfront investment in writing specifications pays off through comprehensive coverage and rapid iteration when bugs are found.

What Solana projects has Certora worked with?

Certora has completed formal verification projects for several major Solana ecosystem players including Jito (the leading MEV infrastructure provider), Kamino (a DeFi protocol), Squads (multi-signature infrastructure), and Manifest. The company has also worked directly with the Solana Foundation on security initiatives. These engagements demonstrate that formal verification is being adopted by sophisticated, high-value protocols that require the strongest possible security guarantees.

How can Solana developers access Certora's services affordably?

Anza has launched a security subsidy program that provides up to one million dollars in funding for Solana builders to access security services. Certora is a participating vendor in this program, meaning developers can potentially receive subsidized access to formal verification, auditing, design reviews, and operational security support. This initiative makes enterprise-grade security accessible to projects that might not otherwise have the budget for comprehensive verification, strengthening the overall security posture of the Solana ecosystem.

What does a formal verification counterexample look like?

When formal verification fails to prove a property, it produces a counterexample—a specific, concrete scenario that demonstrates the violation. In the vault example, the counterexample showed: starting state of 19 assets and 10 shares, a user attempting to redeem 6 shares, and the result of receiving 12 assets when the fair share should have been 11 (since 6/10 of 19 is 11.4, which should round down). This precise counterexample immediately reveals both the existence of the bug and the conditions that trigger it, making fixes straightforward to implement and verify.