RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
Jinhua Wu, Yuting Wang, Liukun Yu, Linglong Meng

TL;DR
This paper introduces RustCompCert, a verified Rust compiler based on CompCert, ensuring semantics preservation and memory safety, simplifying verification of Rust programs.
Contribution
It presents the development of an end-to-end verified Rust compiler that guarantees semantics preservation and memory safety through verifying compilation.
Findings
Semantics preservation from Rust to assembly confirmed
Memory safety ensured by borrow checking pass
Simplifies verification of Rust programs
Abstract
We present our ongoing work on developing an end-to-end verified Rust compiler based on CompCert. It provides two guarantees: one is semantics preservation from Rust to assembly, i.e., the behaviors of source code includes the behaviors of target code, with which the properties verified at the source can be preserved down to the target; the other is memory safety ensured by the verifying compilation -- the borrow checking pass, which can simplify the verification of Rust programs, e.g., by allowing the verification tools focus on the functional correctness.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Testing and Debugging Techniques · Formal Methods in Verification
