Gillian Rust: A hybrid approach to unsafe Rust verification

The Rust Formal Methods Interest group has seen several talks about scalable verification of safe Rust (Prusti, Creusot, Aeneas, Flux…), and other analyses that leverage the guarantees provided by the Rust type and borrow checker (Flowistry, RusSOL…). However, there has been little work on the verification of unsafe Rust, which requires techniques that do not scale as well to large programs. In this talk, we propose a hybrid approach to Rust verification, where safe code is verified by Creusot, and unsafe code is verified by a prototype tool called Gillian-Rust. At the core of this approach is the ability of Gillian-Rust to interpret and verify specifications that Creusot is able to use but not verify.