Formal Verifications

What is formal verification?

Formal verification (FV) is the process of using a formal specification to verify the correctness of a system. The goal of FV is to ensure that a program is free of bugs and meets its requirements.

As of today:

• Squads Protocol v3 was the first program formally verified on Solana. The report made by OtterSec is accessible here.

• Squads Protocol v4 is currently undergoing two independent formal verifications of the new program.

As opposed to a security audit which specifically focuses on identifying security vulnerabilities, Formal verification is a different, mathematical approach to evaluating that a program is working as intended.

When a program is connected to the internet, there is the new risk that bugs may introduce security holes into your system. Even simple buffer overflows can be exploited by skilled attackers to compromise the integrity of a program. Formal verification is one of the most effective methods to ensure a program is free from such vulnerabilities.

OtterSec developed and released the first framework for formally verifying Solana programs in January of this year (2023). They chose Squads Protocol v3 as a case study to showcase the efficacy of this method: https://osec.io/blog/2023-01-26-formally-verifying-solana-programs