Stellar Community Fund

By Formal VerSo

Formal VerSo - Phase 3

SCF #27

$99.9K

Legacy v5.0 Community Award

Awarded

A semi-automated tool for Formal Verification of Soroban contracts using the Software Analysis Workbench (SAW)

Products & Services

Our goal is to democratize formal verification—a technology trusted by industry leaders and governments for their most critical systems—for Soroban developers. This initiative is critical because security flaws in smart contracts have led to billion-dollar losses in recent years. Traditional methods like testing and code review are insufficient, as they cannot cover all inputs and often overlook issues. Instead, we propose an approach based on formal verification to ensure correctness and security of smart contracts. Formal verification leverages rigorous mathematical proofs to eliminate entire classes of bugs and vulnerabilities, beyond the capabilities of traditional testing. A verified contract will always behave as expected even in the presence of malicious actors, ensuring that it has no bugs or vulnerabilities that could cost millions or even billions of dollars.

We will leverage our decades of expertise in formal verification to improve security in Soroban contracts with Formal VerSo (Formal Verification of Soroban contracts). The project will develop formal verification tooling by extending Galois’s Software Analysis Workbench (SAW) with support specific for verifying smart contracts on the Soroban platform. This will allow users of the Soroban platform to ensure their contracts are correct and secure before deploying them. In the decades of developing SAW, Galois has verified critical pieces of software, including Amazon’s S2N cryptography library currently used by hundreds of millions of people. During the activation award, we demonstrated that SAW can be used to formally verify simple Soroban contracts that make straightforward use of just the Soroban storage API. This was done by using SAW’s Rust verification capability and a model of the storage API.

In the upcoming phase, we plan to continue increasing our coverage of the Soroban SDK in the contracts that SAW can verify. This involves incorporating specifications and reasoning principles for various features, including custom types, authentication and authorization and cross contract invocations. Also, since we are now more familiar with the verification process of Soroban contracts, we’ll start paving the way towards a more user-friendly tool with better error reports and better interaction.

Subsequent stages of our work will focus on further expanding our support for the SDK to include more of its features. We also want to start exploring how to make the tool usable and useful for the community. Our overarching objective is to validate the effectiveness of our tool by verifying a real-world, intricate protocol such as the pool-factory of the Blend Protocol. We have engaged with Script3 to start the conversations and plan towards that goal.

You will find the entire roadmap in the technical Architecture document.