Verus 适合验证那些错误代价很高、行为边界清楚的 Rust 核心逻辑，例如权限规则、并发协议、索引结构和关键状态机。它通过规格、前置条件和不变量让开发者说明代码为什么正确。验证能覆盖某些测试难以穷尽的路径，但规格写错、外部系统行为未知或需求本身变化时，仍然需要测试、审查和运行时保护。
形式验证在检查什么
普通单元测试用有限输入检查预期输出。形式验证试图在给定模型与假设下证明性质对所有允许输入成立。开发者需要写出函数需要满足的条件、执行后保证什么，以及循环每次迭代都保持哪些不变量。证明器再检查实现能否满足这些约束。
哪些代码最值得先做
从几十到数百行、边界明确且容易出现极端输入的问题开始效果最好。复杂网络服务的完整行为很难一次建模，服务里的令牌校验、长度计算或队列状态转换则更适合作为入口。先证明一个小模块，可以让团队熟悉规格语言和失败信息。
- 数组索引与长度关系
- 状态机允许的转换
- 排序、去重和集合不变量
- 并发结构的所有权约束
怎样写第一条规格
先把业务规则改写成可判断的句子。比如某个入队操作后，元素数量增加一，旧元素仍可找到，新元素处于队尾。随后把这些句子拆成前置条件、后置条件和循环不变量。
- 先写最小函数及其输入范围。
- 为输出写一个能被调用者使用的保证。
- 遇到循环时写出每轮开始仍为真的性质。
- 让证明器报错后缩小规格或代码范围。
证明失败并不总是实现错误，也可能是规格缺少必要条件。修复前应先判断遗漏的是事实还是假设。
证明和测试如何分工
证明适合处理数学性质和控制流边界，集成测试适合处理数据库、网络、时钟和第三方库。两者不能互相替代。验证模块仍应跑真实编译、模糊测试和接口测试，因为模型与最终运行环境之间可能存在差异。
成本与限制
规格代码需要维护，重构接口后证明也会失效。过于抽象的规格可能证明了一个无用命题，过于贴近实现的规格又会让重构困难。团队应把验证范围写在模块文档中，说明证明依赖哪些假设，避免把局部结论宣传成整个系统已被证明正确。
FAQ
已有 Rust 所有权检查还需要 Verus 吗
需要时仍有价值。所有权主要处理内存和别名约束，业务不变量、算法正确性和协议顺序属于另一类问题。
小团队该从哪里开始
选一个出错会造成明显损失、又不依赖大量外部组件的纯函数或状态机。
团队如何评审验证代码
评审时既要读实现，也要读规格。规格应使用业务术语说明安全条件，让没有参与证明的人也能判断它是否表达了真正需求。对证明依赖的外部假设单独列出，例如输入已经完成校验或底层调用不会失败。这样以后出现事故，团队能迅速辨别是实现破坏了证明，还是证明覆盖范围过小。