一句话：PropProof 自动将 Rust 属性测试框架转换为 Kani 模型检测验证框架，实现低干预的形式化验证。
Rust 开发者常用属性测试（PBT）检查函数正确性，但随机测试只能发现缺陷，无法给出形式化正确性保证。Kani Rust Verifier 虽可基于验证框架进行形式化验证，却要求开发者手写 Kani harness，并需规避内存占用过高、超时等模型检测特有陷阱。本文提出 PropProof，一个自动把 PBT harness 转换为 Kani harness 的库，使已有属性测试可直接用于形式化验证；为此作者设计了若干数据结构模型以优化 Kani 验证框架的性能。该库在 AWS 开发、下载量近 4000 万的 protocol-buffer 库中发现并修复了 2 个问题，并已用于其 CI。基于 42 个来自排名靠前的开源 Rust 库的 PBT harness 的评估表明，PropProof 能让用户以最小人工干预，对现有代码中的复杂用户自定义属性启用 Kani 验证。
Property-based testing (PBT) is often used by Rust developers to test functional correctness properties of their code. Since PBT uses randomized testing, its guarantees are limited: it can detect bugs but provides no formal guarantees of correctness. The Kani Rust Verifier uses the CProver verification framework to verify Rust code, given a specification in a Kani verification harness. However, developers must manually write Kani harnesses while avoiding model-checking-specific pitfalls like large memory usage or timeouts. We introduce , a library that automatically converts PBT harnesses into Kani harnesses which can be formally validated using Kani. We discuss the data-structure models we developed in order to optimize performance of these Kani verification harnesses. Using this library, we identified and fixed 2 issues in , an AWS-developed protocol-buffer library with nearly 40 million downloads. is being used in ’s CI. Our evaluation on 42 PBT harnesses from top-ranked open-source Rust libraries demonstrates enabling the use of Kani to verify complex, user-defined properties on existing code with minimal user intervention.