RefinedRust: A Type System for High-Assurance Verification of Rust Programs

Explore a 17-minute conference talk from PLDI 2024 introducing RefinedRust, a novel refinement type system for high-assurance verification of Rust programs. Delve into the challenges of verifying both safe and unsafe Rust code, and discover how RefinedRust addresses these issues by producing foundational proofs checkable in the Coq proof assistant. Learn about the prototype verification tool implementing RefinedRust, which translates annotated Rust code into a Coq-embedded model and utilizes separation logic automation for type checking. Examine the system's effectiveness through a case study involving the verification of a variant of Rust's Vec implementation, showcasing intricate reasoning about unsafe pointer-manipulating code. Gain insights into the potential impact of RefinedRust on establishing functional correctness in safety-critical systems programmed in Rust.