Sertora presents Sunbeam, a formal verification tool for Soroban smart contracts that uses SMT solvers to mathematically prove code correctness against specifications written in Rust, enabling developers to catch bugs early in the development cycle.
Sertora's Sunbeam is an automated formal verification tool designed specifically for Soroban smart contracts. It takes Soroban code and formal specifications (both written in Rust) as input and either produces a mathematical proof that the code matches the specification or identifies concrete counterexamples demonstrating violations. The tool compiles Rust to WebAssembly, decompiles to an internal representation, applies semantic-preserving transformations, generates verification conditions as logical formulas, and uses SMT solvers like Z3 to check validity. Key advantages over testing include verifying properties for all possible inputs without assuming initial state, and catching bugs early when integrated into CI/CD pipelines. Sunbeam has been used to verify real protocols including Blend V1/V2, Reflector DAO, and Aquarius, with formal verification contests organized through Cantina.
