What formal verification proves
Formal verification uses mathematical methods to prove that a program meets its specification. Unlike security audits, which identify vulnerabilities through manual review and testing, formal verification proves correctness across all possible states. If a property is formally verified, it is mathematically guaranteed to hold.
Formal verification proves specific properties, not general security. Properties not specified and verified could still contain issues. Formal verification complements security audits, it does not replace them.
V4 verification
V4 launched in 2023 and is the current recommended version used by the majority of teams. It has been formally verified by two independent firms using different methodologies.OtterSec
Building on their foundational work with V3 (the first Solana program to be formally verified), OtterSec applied their custom Solana formal verification framework to V4. Their approach translates Solana’s BPF instructions and runtime semantics into formal specifications.Certora
Certora verified V4 using the Certora Prover, which uses formal specifications written in CVL (Certora Verification Language) to describe expected program behavior. The Prover then mathematically proves the implementation satisfies these specifications.Why two independent verifications
Different teams specify properties differently and use different tools, which catches different classes of issues. Agreement between independent verifications strengthens assurance, and the combined scope covers more protocol aspects than either verification alone.Squads Protocol V3 launched in 2022 and is the legacy version, still used by some teams through a separate frontend. V3 was the first Solana program to be formally verified. In January 2023, OtterSec developed the first framework for formally verifying Solana programs and used V3 as the case study. V3 has been immutable since February 2023, so the verified code is exactly what runs onchain. Read the technical blog post.