• Abstract 摘要：提出一种端到端 Rust 验证的混合方法，将证明工作分为对安全 Rust 的强大自动验证和对不安全 Rust 的有针对性的半自动化验证。为此，介绍了 Gillian-Rust，一个基于 Gillian 平台的概念验证半自动化验证工具，可对不安全代码的类型安全性和功能正确性进行推理。Gillian-Rust 为实际 Rust 实现了丰富的分离逻辑，嵌入了 RustBelt 的生命周期逻辑和 RustHornBelt 的参数预言，仅需少量注释就能验证实际 Rust 标准库代码，且验证时间比可比工具快几个数量级。通过为 Creusot（一种先进的安全 Rust 验证器）提供 Creusot 可使用但无法验证的不安全代码规范的系统编码，将 Gillian-Rust 与 Creusot 链接起来，展示了混合方法的可行性。
• Comments 备注：28 页，PLDI'25 论文的扩展版本。
• Subjects 主题：编程语言（cs.PL）。
• Cite as 引用：arXiv:2403.15122 [cs.PL]（或对于此版本为arXiv:2403.15122v3 [cs.PL]），https://doi.org/10.48550/ArXiv.2403.15122，通过 DataCite 发布的 arXiv DOI。
• Submission history 提交历史：由 Sacha-Élie Ayoun 提交，查看邮件，[v1]：2024 年 3 月 22 日星期五 11:24:31 UTC（280 KB），[v2]：2025 年 2 月 10 日星期一 11:07:08 UTC（591 KB），[v3]：2025 年 4 月 10 日星期四 11:04:50 UTC（431 KB）。