---
id: 5686
title: "Solana formal verification: a case study"
source_domain: osec.io
source_url: "https://osec.io/blog/formally-verifying-solana-programs/"
published_at: "2023-01-26T00:00:00Z"
tags: ["rust", "formal-verification", "solana", "anchor", "kani", "squads"]
phying_url: "https://phying.com/item/5686"
lang: en
---

# Solana formal verification: a case study

## Summary

OtterSec presents a framework for formal verification of Solana Anchor programs — autogenerated proof harnesses checked by the Kani verifier — with a Squads multisig case study.

## Intelligence Metadata

- **Sources:** osec.io
- **Published:** 2023-01-26T00:00:00Z
- **Original:** https://osec.io/blog/formally-verifying-solana-programs/
- **Phying News:** https://phying.com/item/5686