用 Verus 为 Rust 代码编写可证明正确的程序

Verus 是面向 Rust 的开源自动化程序验证器，开发者可在 Rust 源码中直接添加规范与证明，工具自动完成大量底层证明步骤，通常 1 秒内返回反馈，并可在 VS Code 中以红波浪线提示错误。Verus 已用于验证 Nitro Isolation Engine 的关键原语及 Amazon 内部多项核心基础设施，其自动化与快速反馈也便于 AI 智能体迭代生成证明。