Verifying Rust programs with Creusot

January 26 2026 - 00:00UTC

Creusot is a deductive verifier for Rust. In this talk, I will present Creusot's newest features and case studies. One notable addition is the support for linear ghost resources (inspired by Verus), which enables the verification of unsafe Rust code involving raw pointers. Applications include verified implementations of union-find and persistent arrays (CPP 2026), as well as the verification of slice functions in the Rust standard library (ongoing work towards the verify-rust-std challenge).

Speaker: Li-yao Xia, research engineer at Laboratoire Méthodes Formelles.