作者：Rémi Delmas，Zyad Hassan，秦和平，Rahul Kumar，Felipe R. Monteiro，Thanh Nguyen，Adrián Palacios，Celina Val，Michael Tautschnig，Justus Adam，Daniel Schwartz-Narbonne，Carolyn Zech 查看 PDF HTML（实验性） 摘要：Rust 的所有权类型系统防止安全代码中的内存错误，但某些期望的属性仍然与编译正交：不安全操作的健壮性（例如，原始指针解引用）、功能正确性和运行时无恐慌。我们提出 Kani，一个开源的 Rust 模型检查器，它将有界模型检查推向超越错误查找，为这些属性提供正确性保证。Kani 从 Rust 的中级中间表示（MIR）编译证明工具，进入 CBMC 的位精确验证引擎，自动检查一整套安全属性，无需用户注释。为了将验证从有界扩展到无界，Kani 提供了一种规范语言，包括函数契约、循环契约、量词和函数存根。我们通过对工业 Rust 项目的案例研究证明了其可行性，其中合同将验证从无恐慌提升到功能正确性，发现了六个之前未知的错误。Kani 在生产 CI 中大规模运行，在 Rust 标准库验证活动中，每次代码更改验证超过 16,000 个工具。 评论：已接受于第 39 届 IEEE/ACM 自动化软件工程国际会议（ASE 2026），行业展示轨道 主题：软件工程（cs.SE）；计算机科学中的逻辑（cs.LO）；编程语言（cs.PL） ACM 类别：D.2.4；F.3.1 引用为：arXiv:2607.01504 [cs.SE]（或 arXiv:2607.01504v1 [cs.SE] 为此版本） https://doi.org/10.48550/arXiv.2607.01504 arXiv 发布的 DOI 通过 DataCite（待注册） 提交历史 来自：Felipe R. Monteiro [查看电子邮件] [v1] 2026 年 7 月 1 日 星期三 22:05:33 UTC（149 KB）