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.