Alerus Brings Formal Verification to Probabilistic Rust Code
Alerus extends Verus with error-credit reasoning to formally verify randomized sampling algorithms in real Rust code, with soundness proved in Rocq.
A new framework called Alerus extends formal verification to probabilistic algorithms written in real-world Rust, closing a long-standing gap where prior tools only worked on idealized, verification-specific languages. Built on top of Verus—Rust's SMT-based verifier with separation-logic reasoning—Alerus adds probabilistic capabilities without sacrificing Verus's existing automation.
The key mechanism is a lightweight 'error credit' construct, a ghost-state technique borrowed from the Eris program logic, which lets developers specify and prove correctness properties for randomized sampling routines. The paper demonstrates this on practical samplers including discrete Gaussian distributions, the alias method, and the fast loaded dice roller—algorithms commonly used in cryptography and statistical computing.
Soundness of the extension is established by adapting VerusBelt, a logical-relations model of Verus expressed in Iris separation logic, swapping in Eris's probabilistic weakest precondition. The entire soundness proof is mechanized in Rocq, giving engineers a rigorously verified path to trust randomized code shipped in production Rust systems.