代码大模型 / AI 编程

KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code

KVerus：面向Rust代码的可扩展且高鲁棒性的形式化验证证明生成工具

Yuwei Liu, Xinyi Wan, Yanhao Wang, Minghua Wang, Lin Huang, Tao Wei

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.SE

AI总结 KVerus是适配Rust代码的形式化验证工具，通过自适应范式与动态知识库，在单文件、仓库级基准及Rust内核验证中均优于现有方案，为形式化验证的规模化应用提供了关键进展。

Comments Accepted at ASE 2026