# Formal Verifications

{% hint style="info" %}
**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.
{% endhint %}

As of today:&#x20;

* Squads Protocol v3 was the first program formally verified on Solana. The report made by OtterSec is accessible [here](/main/security/formal-verifications/squads-protocol-v3.md).&#x20;
* Squads Protocol v4 is formally verified by [two independent auditors](/main/security/formal-verifications/squads-protocol-v4.md).

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.&#x20;

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>&#x20;


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.squads.so/main/security/formal-verifications.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.
