RefinedRust: A Type System for High-Assurance Verification of Rust Programs
summary
RefinedRust presents a refinement type system that verifies both unsafe Rust and safe Rust by translating MIR into a Coq-embedded Rust model and checking properties with separation-logic automation, producing foundational Coq proofs that need no trusted external checker. A prototype verifies a Vec variant: about 120 lines of Rust expand to ~1,000 lines in the operational model, specifications stay small, and new ideas like borrow names and place types track mutable borrows and intermediate states.
AI-written summary · about
chapters (13)
- 0:00RefinedRust for Rust verification
- 1:04Verifying unsafe Rust code
- 2:52RefinedRust: RustBelt and RefinC
- 4:36User workflow with RefinedRust
- 5:36Example: add_42 verification
- 6:40Verifying unsafe Vector library
- 8:44Mutable references in RefinedRust
- 10:53Verification limits and automation
- 11:56Case study results and performance
- 12:16Scaling RefinedRust for practice
- 13:00RefinedRust paper details
- 13:22Place types for Rust states
- 15:29Summary and open questions
related talks
19mA Hybrid Approach to Semi-automated Rust Verification
14mA Refinement Methodology for Distributed Programs in Rust
21m“Fearless Refactoring & the Art of Argument-Free Rust”
18mVerus: Verifying Rust Programs using Linear Ghost Types
20mVerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)
21mA Tour of Empirical Verification in Rust
58mRust for The Curious C++ Developers
19mRavencheck: Effectively-Propositional Reasoning for Rust