RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code
summary
RustHornBelt gives a formal, mechanized bridge between RustHorn-style automatic specs and RustBelt’s unsafe-code semantics: a Coq model built on Iris separation logic and a predicate-transformer type-spec system, plus a Coq mechanization proving soundness for RustHorn specs linked to unsafe implementations. It implements and verifies key APIs (Vec push and index_mut, Mutex, Cell) using parametric prophecies (a clairvoyant monad) to model mutable borrows, resolves prophecies at borrow release, and reports completed machine-checked proofs that the verified unsafe APIs soundly compose with automatic verification.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:37Our High-level Goal: Rust Verification
- 1:38Two Lines of Prior Work on Rust Verification
- 3:39Our Work, RUSTHORNBELT
- 4:35Motivating Example for RUSTHORN
- 6:11RUSTHORN – Automated Verification
- 8:21Type-Spec System
- 9:01RUSTHORN-style Representation of Rust Objects
- 11:40RUSTHORN's Spec for push
- 12:40RUSTHORN's Spec for index_mut
- 13:53Parametric Prophecies
related talks
20mVerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)
19mA Hybrid Approach to Semi-automated Rust Verification
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
20mModular Specification and Verification of Closures in Rust
15mModular Specification and Verification of Closures in Rust
59mWhat's the deal with unsafe Rust?
15mAeneas: Rust Verification by Functional Translation
19mRavencheck: Effectively-Propositional Reasoning for Rust