A hybrid approach to semi-automated rust verification
File(s)
Published version
Author(s)
Ayoun, Sacha-Élie
Denis, Xavier
Maksimović, Petar
Gardner, Philippa
Type
Journal Article
Abstract
We propose a hybrid approach to end-to-end Rust verification where the proof effort is split into powerful automated verification of safe Rust and targeted semi-automated verification of unsafe Rust. To this end, we present Gillian-Rust, a proof-of-concept semi-automated verification tool built on top of the Gillian platform that can reason about type safety and functional correctness of unsafe code. Gillian-Rust automates a rich separation logic for real-world Rust, embedding the lifetime logic of RustBelt and the parametric prophecies of RustHornBelt, and is able to verify real-world Rust standard library code with only minor annotations and with verification times orders of magnitude faster than those of comparable tools. We link Gillian-Rust with Creusot, a state-of-the-art verifier for safe Rust, by providing a systematic encoding of unsafe code specifications that Creusot can use but cannot verify, demonstrating the feasibility of our hybrid approach.
Date Issued
2025-06-01
Date Acceptance
2025-03-06
Citation
Proceedings of the ACM on Programming Languages, 2025, 9 (PLDI), pp.970-992
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
970
End Page
992
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
9
Issue
PLDI
Copyright Statement
© 2025 Owner/Author. This work is licensed under Creative Commons Attribution International 4.0.
License URL
Publication Status
Published
Article Number
186
Date Publish Online
2025-06-13