用 Verus 写出可证明正确的 Rust 代码
来源: amazon.science — 2026-08-31
概述
亚马逊科学博客介绍了开源程序验证器 Verus：它针对功能的形式化数学规约，机械地检查代码在所有可能输入下是否满足，从而超越传统测试、覆盖边界情况。开发者用类 Rust 语法直接在源码里写前置与后置条件，反馈循环不到一秒，还能让 AI 代理协助生成证明。Verus 可以对 Rust 的 unsafe 代码块以及使用自定义锁方案的并发代码做数学验证，重新建立机器检查的安全保证，AWS Nitro 隔离引擎的关键组件就靠它验证。
核心要点
- Verus 机械地检查代码对全部可能输入是否满足形式化数学规约，比测试更能抓住角落情况。
- 规约直接写在 Rust 源码里，反馈循环不到一秒，也便于 AI 代理参与生成证明。
- 它能验证 Rust 的 unsafe 代码块以及使用自定义锁方案的并发代码。
- 应用场景包括 AWS Nitro 隔离引擎的关键组件，用于提升安全性保证。
- 已被开源项目采用，覆盖证书校验库、数据格式解析器与 Kubernetes 控制器等分布式系统。
金句
它机械地检查代码是否满足形式化数学规约，从而超越传统测试。
👍 0
👎 0
返回 Lobsters 首页