该论文介绍了Kani，一个针对Rust代码的模型检查器。Rust的所有权类型系统能防止安全代码中的内存错误，但无法保证不安全操作的正确性、功能正确性及运行时错误缺失。Kani通过模型检查填补了这一空白。

Kani：一款针对Rust语言的模型检测工具

Rust的所有权类型系统能确保安全代码中无内存错误，但某些关键属性仍无法通过编译保证，例如不安全操作（如原始指针解引用）的正确性、功能正确性以及运行时恐慌的避免。为此，我们推出Kani——一款面向Rust的开源模型检测工具。它将有界模型检测从单纯的漏洞查找提升至正确性验证，能够针对上述属性提供保障。Kani将Rust的中间级中间表示（MIR）中的证明测试框架编译至CBMC的位精确验证引擎，无需用户标注即可自动检查全面的安全属性。为将有界验证扩展至无界验证，Kani提供了一套规范语言，包含函数契约、循环契约、量词和函数桩。我们通过工业级Rust项目的案例研究验证了其可行性：在契约的辅助下，验证从仅关注无恐慌状态升级为功能正确性验证，并发现了六个此前未知的漏洞。Kani已在生产环境的持续集成中大规模运行，在Rust标准库验证活动中，每次代码变更需验证超过16,000个测试框架。

根据评论内容，主要观点和论据如下：

1. 工具资源与教程分享（评分：无） - 评论1提供了相关论文链接（"Their old paper"） - 评论2分享了Kani教程（"The tutorial is helpful"）并类比hypothesis-auto工具（"Reminds me a bit of hypothesis auto"）

2. 相关工具对比（评分：无） - 评论3指出另一个Rust模型检查工具更专注于并发bug检测（"A related Rust model checking tool more focused on detecting concurrency bugs"） - 评论4引用2022年关于Kani Rust验证器的讨论（"Kani Rust Verifier – a bit-precise model-checker for Rust"）

3. 讨论平衡性：评论内容以资源分享和工具对比为主，未出现明显对立观点。所有评论均未提供评分，因此无法基于认可度进行权重分析。整体呈现技术社区常见的工具推荐与信息补充模式。