一句话：提出将 Rust 验证分为自动验证安全代码与半自动验证 unsafe 代码的混合方法，并实现 Gillian-Rust 与 Creusot 联动。
该论文针对端到端 Rust 验证中 unsafe 代码难以自动验证的问题，提出一种混合验证方法：对安全的 Rust 代码使用强自动化验证，而对 unsafe Rust 则进行有针对性的半自动化验证。作者在 Gillian 平台之上构建了原型工具 Gillian-Rust，它将 RustBelt 的生命周期逻辑与 RustHornBelt 的参数化预言嵌入到一个面向真实 Rust 的丰富分离逻辑中，从而能够推理 unsafe 代码的类型安全与函数正确性。评估表明，该工具只需少量标注即可验证真实 Rust 标准库代码，且验证时间比同类工具快多个数量级。论文还通过系统化编码 unsafe 代码的规约，使其可被安全 Rust 验证器 Creusot 使用（尽管 Creusot 本身无法验证这些规约），从而展示了该混合方法的可行性。
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.
@article{paperbot3110,
title = {A Hybrid Approach to Semi-automated Rust Verification},
author = {Sacha-Élie Ayoun and Xavier Denis and Petar Maksimović and Philippa Gardner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729289}
}