Verus：一款用于验证 Rust 代码正确性的静态分析工具

Verus 是一款用于验证 Rust 代码正确性的静态分析工具。开发者编写代码规范，Verus 静态检查可执行 Rust 代码是否始终满足所有可能执行情况下的规范。它不依赖运行时检查，而是依靠强大的求解器来证明代码的正确性。Verus 目前支持 Rust 的子集（正在扩展中），在某些情况下，它允许开发者超越标准 Rust 类型系统，静态检查例如操作原始指针的代码的正确性。Verus 仍在积极开发中，功能可能存在问题或缺失，文档也不完整。