Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust

Explore advanced deductive verification techniques in Rust through this 21-minute conference presentation from CPP 2026. Learn how researchers from Université Paris-Saclay extended the Creusot verification tool with linear ghost resources to handle Rust's interior mutability challenges. Discover how the "shared xor mutable" principle in Rust's type system, while beneficial for verification, creates obstacles when programs need to circumvent it through interior mutability mechanisms. Examine the implementation of ghost ownership concepts, building upon previous work in the Verus tool, and see how Creusot's full support for mutable borrows enables enhanced specifications for linear ghost code primitives. Follow detailed case studies demonstrating the practical application of this methodology to verify two complex data structures that require both sharing and mutation: union-find algorithms and persistent arrays. Gain insights into how linear ghost resources provide a systematic approach to reasoning about programs that use interior mutability, advancing the state of formal verification for systems programming in Rust.