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)
