Muli Sagif, CEO of Certora, discusses formal verification for smart contracts and announces Soroban support for their verification platform at Meridian in Madrid. Certora is expanding beyond EVM to WebAssembly and Rust, bringing formal verification tooling to the Stellar ecosystem.
In this Tech Talks interview at Meridian, Tomer from the Stellar Development Foundation speaks with Muli Sagif, CEO of Certora, about formal verification in blockchain. Sagif traces his journey from academic formal verification research to building Certora, which has become a leading smart contract auditing platform used by major projects like Compound and MakerDAO. The discussion covers why smart contracts are ideal for formal verification, the challenges of EVM semantics and nonlinear arithmetic, and Certora's evolution from a tool-focused company to a broader security platform. The major announcement is Certora's first WebAssembly support through Soroban integration, enabling verification for Rust-based contracts. Sagif explains how formal verification differs from fuzzing by providing exhaustive proofs rather than probabilistic testing, and discusses future plans including incident response services, verification competitions, and a new specification language called CDL to decouple specs from code.
