用 Verus 让 Rust 代码获得数学级正确性
Developing provably correct Rust code with Verus
Rust 语言虽然凭借类型系统大幅减少了内存错误，但“更安全”并不等同于“绝对正确”。Amazon 推出的开源工具 Verus，作为 Rust 的自动化程序验证器，能够将代码与数学规格进行机械比对，从而验证所有可能输入下的正确性。开发者只需在源码中直接添加前置和后置条件，Verus 即可在秒级内完成验证，甚至支持 AI 辅助生成证明。从 AWS 的 Nitro Isolation Engine 到 Kubernetes 控制器，Verus 正帮助关键基础设施在保留 Rust 高性能的同时，重新建立机器可验证的安全保障，将软件验证从“测试覆盖”推向“数学证明”的新高度。
Rust 无法保证你的程序会计算出你期望的结果，也无法保证它不会泄露其访问的秘密。
HN 评论区
76- 63
如果你觉得这个有趣，可能也会对一些目标/范围相似的相关项目感兴趣：Miri[0]、Kani[1] 和 Creusot[2]。Verus、Kani 和 Creusot 之间看起来有相当多的重叠，但我没用过其中任何一个，所以就不试图去区分它们了。
[0]https://github.com/rust-lang/miri
- sourdecor
Verus 看起来正是我一直在寻找的东西！我前段时间在 HN 上发现了 AllConcur[0]，本想把它移植到 Go，但它用了 TLA+ 和 C，对我来说很难理解，除非能把 TLA+ 编译成 C，否则很难让人信任其实现。
我和 Gemini 聊过 Verus 与 TLA+ 的对比，它说 TLA+ 通常用于（例如）“证明分布式共识协议在逻辑上是健全的”，但当我问 Verus 是否也能做到时，它说可以。所以 Verus 可以编译并集成到 Rust 中，而 TLA+ 更多用于蓝图开发，随后由实现者在脑海中指导具体实现。
太棒了！
- MeetingsBrowser
我长期以来一直批评那些需要注解的验证工具。人类都写不出正确的代码，那要求他们写出正确的证明注解似乎徒劳无功。
但在 LLM 时代，情况或许会改变。一种确定性检查可以让 LLM 验证 API 的正确性，从而大幅提高大规模重构或性能优化的成功率。
令人兴奋！
- freethinky
有人知道有没有类似的东西存在，并且被用于 .NET/C#，而且还在积极维护？不要像 Dafny 那样需要我用另一种语言写（我公司大概率不会允许）。另外最好是注解形式的（这样我就能直接开始用了）。
- nottorp
这对新改进版 ubuntu coreutils 里的 bug 有帮助吗？