Verus —— 用于验证 Rust 代码正确性的工具

Verus 是一款用于验证 Rust 代码正确性的工具。开发者编写代码功能规范，Verus 会静态检查可执行的 Rust 代码是否始终满足所有可能执行场景下的规范。

Verus 并非添加运行时检查，而是依靠强大的求解器来验证代码的正确性。Verus 目前支持 Rust 的一个子集（开发团队正在努力扩展），在某些情况下，它允许开发者超越标准 Rust 类型系统，静态检查代码的正确性，例如操作原始指针的代码。

Verus 的目标是：

• 提供纯数学语言来表达规范（如 Dafny、Creusot、F*、Coq、Isabelle/HOL）
• 提供一种基于经典逻辑（如 Dafny）的数学语言来表达证明（如 Dafny、F*、Coq、Isabelle/HOL）
• 提供一种基于 Rust（如 Prusti、Creusot 和 Aeneas）的低级、命令式语言来表达可执行代码（如 VCC）
• 根据以下原则， 生成小型、简单的验证条件，以便Z3等 SMT 求解器能够有效地解决这些条件：
  • 使数学规范语言接近 SMT 求解器的数学语言（如 Boogie）
  • 使用轻量级线性类型检查（而不是 SMT 求解）来推理内存和别名（例如 Cogent、Creusot、Aeneas 和线性 Dafny）