Stellar Community Fund

By Formal VerSo

Formal VerSo

SCF #20

$50.0K

Legacy v5.0 Activation Award

Awarded

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

Products & Services

Security vulnerabilities in smart contracts have cost billions of dollars over the last few years. Preventing vulnerabilities and ensuring correct, intended behavior of smart contracts could thus save billions of dollars. The traditional approach to software security and correctness is based on testing and code review, but testing cannot cover all possible inputs and code review often misses problems. 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.

The Formal VerSo (Formal Verification of Soroban contracts) project will develop formal verification tooling for Soroban by extending Galois’s Software Analysis Workbench (SAW) with support for verifying smart contracts on the Soroban platform. This will allow users of the Soroban platform to make sure their contracts are correct and secure before deploying them. Galois has decades of experience developing SAW and applying it to perform formal verification, including working with Amazon to formally verify their S2N cryptography library. Galois has recently developed SAW support for formal verification of Rust programs, such as the Rust programs used to write Soroban contracts. This first phase of the Formal VerSo project, for the activation award, will demonstrate how SAW can be used to formally verify simple and small Soroban contracts by treating them as standard Rust programs. Later phases of the work will then develop reasoning principles specific to the Soroban platform and API, allowing more complex Soroban contracts to be verified.