Formal verification checks whether code satisfies precisely stated properties within a defined model and set of assumptions. This guide explains what that means for smart contracts, how it complements testing and human audits, and what a verification engagement involves. A flaw found in Solana’s SPL Stake Pool shows how a property can expose a consequential edge case before deployment.

Certora verified the security of Solana's core upgrade from SPL Token to the optimized P-Token program. We used the Certora Solana Prover to prove their equivalence, ensuring that P-Token is a safe drop-in replacement.

Formal verification, testing, and smart contract audits address different questions about protocol security. This guide compares the risks each method can uncover, the limits of a clean result, and how to combine them throughout development, launch, and upgrades. Real protocol examples show why coverage depends on review scope, tested inputs, stated properties, and model assumptions.

We examine four ways formally verified systems can fail: incorrect specifications, flawed assumptions, mismatches between verified models and deployed code, and bugs in verification tools themselves. Through real-world examples, we explain how to identify these risks and what to check before relying on a formal verification proof.