一句话：扩展 RefinedRust 以支持 trait、闭包和迭代器等高级抽象并与 unsafe 代码结合，从而对真实 Rust 代码进行基础验证。
Rust 的内存安全保证使其适合安全关键系统，但功能正确性仍需演绎验证。RefinedRust 是支持 unsafe 指针操作并在 Rocq 中生成机器检查证明的基础验证工具，但缺少 trait、闭包、迭代器等真实代码常用高级抽象，且这些抽象此前未被基础验证工具支持。本文扩展 RefinedRust，为这些特性提供验证支持，并保证它们可与 unsafe 代码协同使用。作者通过验证真实低层 ACE 安全监控器内存子系统的若干关键部分（包括页分配器）来展示扩展的有效性，表明基础验证能处理实际 Rust 系统代码。
Rust is a modern systems programming language that, thanks to its strong memory safety guarantees, is well-suited to the domain of safety-critical systems. Since memory safety alone is not ultimately enough for safety-critical systems, there have emerged in recent years a number of tools for deductive verification of functional correctness of Rust programs. One recent tool, RefinedRust, is notable in that it both handles unsafe pointer-manipulating Rust code and produces foundational, machine-checked proofs in the Rocq prover. However, RefinedRust is a prototype tool and lacks support for several of the high-level abstractions that Rust provides, including traits, closures, and iterators. These features are commonly used in real-world Rust code, and are supported by other non-foundational Rust verification tools like Prusti and Creusot. In this paper, we show how to extend RefinedRust with these features, and in a manner such that they can be used in conjunction with unsafe code. We demonstrate its usefulness by verifying interesting parts of the memory subsystem of the real-world, low-level ACE security monitor, including its page allocator.
@article{paperbot12147,
title = {Bringing Foundational Verification to Real-World Rust Code},
author = {Lennard Gäher and Vincent Lafeychine and Sascha Kehrli and Avraham Shinnar and Wojciech Ozga and Guerney Hunt and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839484}
}