verus-lang/verus

项目用途

Verus 用来验证 Rust 代码是否符合开发者写下的规格。开发者为函数声明前置条件和后置条件，Verus 借助求解器做静态分析，证明可执行代码在所有可能的执行路径上都满足这些规格。它不是运行时断言库：检查发生在验证阶段，通过后代码仍按普通 Rust 方式运行（在支持的子集内）。

Verus 目前支持 Rust 的一个子集，并在持续扩展。由于验证不局限于标准类型系统，它也能推理操作裸指针等底层写法，因此面向系统级代码。README 明确标注项目处于活跃开发中，功能可能缺失或不稳定，文档也不完整。

快速开始

想先体验，可以直接打开浏览器里的 Verus Playground，无需本地安装。正式开发则按安装说明配置环境，再阅读教程与参考手册。

带验证的函数把契约写在签名里：

fn octuple(x1: i8) -> (x8: i8)
    requires
        -16 <= x1,
        x1 < 16,
    ensures
        x8 == 8 * x1,
{
    let x2 = x1 + x1;
    let x4 = x2 + x2;
    x4 + x4
}

这个例子来自 Hacker News 评论，用来展示写法，并非安装步骤的一部分。实际使用时，把规格和实现写在 Verus 注释的 Rust 文件中，运行验证器，得到证明成功或指向反例的错误报告。具体命令、工具链版本和编辑器集成以安装说明为准，README 没有重复这些细节。

使用约束

• Rust 子集：并非所有 Rust 语法都能通过 Verus，部分语言特性尚不支持，支持范围仍在扩大。
• 文档成熟度：文档被描述为进行中，遇到问题需要到 Zulip 社区求助。
• 规格成本：编写契约、调试失败的证明是工作流程的一部分；验证只证明你写下的规格，规格本身不准确或不完整会限制结论的意义。
• 生态配套：发布经过验证的 crate 到 crates.io 有单独的实践指南；代码格式化由独立的 verusfmt 提供。
• 许可证：仓库采用 MIT 许可证。

HotRepo 点评

Verus 在 2024 年 5 月登上 Hacker News 讨论，获得 284 分和 103 条评论。讨论中最具体的采用案例是 lsuresh 提到用 Verus 编写经过形式化验证的 Kubernetes 控制器，并证明「控制器最终会把集群调和到期望状态」这类活性属性，同时给出了代码和 OSDI 2024 论文。这类描述比笼统称赞更有参考价值，因为它点明了被证明的性质以及规格本身就很微妙的领域。讨论也暴露了一个实际摩擦点：有评论者指出 Verus 要求把代码包在 proc-macro 中，而 Creusot 等工具采用属性式语法，在 Rust 里更轻量、更符合习惯。站内最近一条 Rust 语言日榜快照是 2026-11-14，显示 3,768 星、当日新增 20 星、该榜第 3 名；单条快照只能说明当天情况，不足以判断趋势。

项目源码与说明