本文永久链接 – https://tonybai.com/2026/10/18/verus-rust-formal-verification-amazon-nitro

大家好，我是Tony Bai。

【导读】

Rust的类型系统能防内存越界、防数据竞争，但它证明不了“代码算出来的结果是对的”。亚马逊选择用一套叫Verus的开源工具，把Rust代码直接变成可以被数学证明的对象——不用切换语言，不用另起炉灶，甚至连unsafe代码和并发锁都能证明“绝对正确”。这套武器已经被用在AWS Nitro隔离引擎的核心组件上。

【文章要点】

  • Rust安全≠正确：内存安全只是底线，Verus要证明的是代码在所有可能输入下都符合规约，而不是测试用例覆盖到的那几个场景；
  • 规约直接写进Rust源码：用requires/ensures标注前置与后置条件，普通Rust编译器会忽略这些标注，验证代码照样能被Cargo正常编译发布；
  • 秒级反馈，AI也能参与证明：自动求解器负责繁琐的底层证明步骤，人类只需提供高层提示，这也让AI Agent有了介入证明生成的空间；
  • 能啃unsafe和并发这两块硬骨头：Verus可以为脱离编译器保护的unsafe代码、自定义锁机制重新建立机器可检查的安全保证；
  • 已经走出亚马逊：证书校验库、数据格式解析器、Kubernetes控制器等一批开源项目都已经引入Verus。

Rust已经很安全了，亚马逊为什么还不满足

这些年，Rust凭借接近C语言的性能，加上编译期就能拦截内存错误的类型系统，已经拿下了不少工业界的关键基础设施。在亚马逊内部，Firecracker（支撑AWS Lambda和Fargate的微虚拟机方案）、内部的无服务器分布式SQL数据库，以及为Nitro Hypervisor提供虚拟机隔离能力的Nitro隔离引擎，都是用Rust构建的。

但“更安全”不等于“绝对正确”。举一个最直观的例子：在C语言里，数组越界访问是一个后果完全不可预测的危险操作；换到Rust里，越界访问会让程序直接崩溃退出，这确实比C语言的“未定义行为”安全得多。可问题是，一段真正正确的代码，压根就不应该走到“越界访问”这一步——无论是崩溃还是继续跑下去，都说明代码本身有问题。

同样的道理，Rust的类型系统也无法保证程序算出来的结果就是开发者预期的那个结果，更无法保证程序不会意外泄露它能访问到的敏感数据。这些问题已经超出了编译器和类型系统的检查能力范围，需要另一套武器来解决——这就是Verus登场的地方。

Verus是什么：把数学证明搬进Rust源码

Verus是一个开源的、面向Rust的自动化程序验证器。所谓“程序验证器”，指的是这样一类工具：你先给出一份关于代码应该如何运行的数学规约（specification），验证器再机械地检查代码在所有可能的输入下都满足这份规约。

举个例子：假设你写了一个优化过的二分查找函数，用来在一个有序数组里定位目标值。对应的规约可能是——如果函数成功返回了一个下标，那么数组里这个下标对应的元素必须正好等于目标值。而Verus要做的，就是对所有可能的数组和所有可能的目标值，机械验证这条规约始终成立。

这和传统测试有本质区别。测试只能挑几组具体的数组和目标值去跑一遍，很容易漏掉边界情况——比如目标值恰好是数组最后一个元素，或者目标值根本不在数组里。而形式化验证要求构造出一份严谨的数学证明，证明代码在任意输入下都不会违反规约。

在Verus这样的自动化验证器里，绝大部分繁琐、机械的证明步骤由工具自动完成，开发者只需要提供高层次的引导，比如搭建一个归纳证明的框架，或者补充一个循环不变式。而如今，就连这些高层引导，很多时候也已经可以交给AI来完成。

下面是一张简化的Verus工作流程示意图：

亚马逊是Rust基金会的创始成员之一，在Rust上的投入由来已久；再加上亚马逊在自动化推理领域已经积累了超过十年的经验，选择在Rust项目里引入Verus，几乎是水到渠成的事情。目前，亚马逊已经用Verus证明了Nitro隔离引擎所依赖的若干关键组件的正确性，也验证了内部其他一些关键基础设施。

代码怎么写：一个二分查找的规约示例

Verus最与众不同的一个设计决策是：规约和证明都直接写在Rust源码里，语法风格也尽量贴近Rust本身。开发者不需要另外学一门规约语言，验证失败时看到的报错信息也是Rust风格、定位到具体源码行的。更重要的是，写代码的人往往就是最懂这段代码的人，让他们直接参与证明过程，比另外找一批专职的验证工程师要高效得多。

下面是一段示意性质的伪代码，模拟了Verus为二分查找函数标注前置/后置条件的方式（并非原文截图，仅用于说明思路）：

// 示意代码：为二分查找函数标注Verus规约
verus! {

fn binary_search(arr: &[i32], target: i32) -> (result: Option<usize>)
    requires
        // 前置条件：数组必须是非降序排列的
        forall|i: int, j: int| 0 <= i < j < arr.len() ==> arr[i] <= arr[j],
    ensures
        // 后置条件一：若返回了下标，该下标必须合法，且对应元素等于目标值
        result matches Some(idx) ==> idx < arr.len() && arr[idx as int] == target,
        // 后置条件二：若返回None，说明目标值确实不存在于数组中
        result matches None ==> forall|i: int| 0 <= i < arr.len() ==> arr[i] != target,
{
    // 具体实现省略
    unimplemented!()
}

} // verus!

这里有两个细节值得注意：

第一，requires标注的是前置条件——本例中要求数组必须有序，这是二分查找算法成立的前提；ensures标注的是后置条件——不仅规定了返回Some(idx)时下标必须合法且对应元素匹配，还专门规定了返回None时目标值必须确实不在数组中。第二条后置条件容易被忽略，但它至关重要：如果没有这一条，一个永远返回None的“假二分查找”也能满足规约，因为它确实从不会返回错误的下标。

第二，requires、ensures、forall这类写法并不是合法的stable Rust语法，光靠标准rustc是编译不过的。Verus的做法是把这套规约语法包装进verus!这个宏里——这个宏由verus_builtin_macros等正式发布在crates.io上的proc-macro包提供。当项目只用普通stable Rust加Cargo编译、不经过Verus验证器本身时，这个宏会执行“幽灵代码擦除”（ghost erasure）：把纯规约、纯证明的部分从展开结果里剥离掉，只保留真正会运行的可执行逻辑，最终生成一份合法、能被stable rustc正常编译的Rust代码。

这不是纸上谈兵，可以实际验证。只依赖verus_builtin和verus_builtin_macros这两个真实发布的crate（不装Verus验证器，只用普通stable rustc），写一个带requires/ensures的函数：

注：在cargo工程里通过cargo add添加verus_builtin和verus_builtin_macros两个crate依赖。

use verus_builtin_macros::verus;
use verus_builtin::*;

verus! {

fn add_one(x: u32) -> (y: u32)
    requires
        x < 100,
    ensures
        y == x + 1,
{
    x + 1
}

} // verus!

fn main() {
    let r = add_one(41);
    println!("add_one(41) = {}", r);

    // 故意用一个违反requires(x < 100)前置条件的输入调用函数，
    // 看普通cargo build/run（未经过Verus验证器）会不会在运行时报错
    let r2 = add_one(9999);
    println!("add_one(9999) = {} （违反了requires，但仍正常返回）", r2);
}

用普通cargo build加stable rustc编译，完全没有任何报错，cargo run的输出是：

add_one(41) = 42
add_one(9999) = 10000 （违反了requires，但仍正常返回）

第二行是关键：传入9999明显违反了requires x < 100，但由于没有经过Verus验证器，代码在普通编译运行下完全没有把requires/ensures变成任何运行时检查——这两句规约被整段擦除了，而不是变成了一次assert!。翻一下verus_builtin_macros的源码也能看到确认这一点的逻辑：

#[cfg(not(verus_keep_ghost))]
pub(crate) fn cfg_erase() -> EraseGhost {
    EraseGhost::EraseAll
}

也就是说，只要没有设置verus_keep_ghost这个cfg标志（普通cargo build默认就不会设置），宏在展开阶段就会把所有规约、证明相关的代码整体擦除，只留下真正会被编译执行的那部分逻辑。同一份源码，能被没有安装Verus验证器的项目通过标准Cargo正常消费，但前提是项目要显式依赖这些Verus配套crate——验证能力更像是一层可以按需叠加的“加分项”，而不是必须绕开的硬门槛。

快在哪里：秒级反馈和AI辅助证明

Verus的另一个核心卖点是自动化程度高、反馈速度快。它背后依赖多种自动求解器（solver），负责把代码和规约转化出的证明义务自动“消化”掉。实际使用中，开发者写代码和证明后，通常能在一秒以内拿到反馈——这个速度足以支撑起交互式开发体验，比如在VS Code这类编辑器里像看到语法错误的红色波浪线一样，实时看到证明是否通过。

放到项目级别看，这种自动化的威力更明显：一些体量达到数千行代码加证明的复杂项目，Verus完成验证所需的时间，在过去一些早期自动化验证工具那里，可能只够验证单个函数。

这种“又快又省人力”的特性，不仅方便了人类开发者，也顺势打开了AI参与证明的大门——自动化程度越高，AI Agent需要自己动手补全的证明细节就越少，迭代速度自然也就越快。这或许也是形式化验证在AI辅助编程时代重新被重视的原因之一：过去写证明的门槛太高，现在人和AI可以一起把这道门槛降下来。

撬开两块硬骨头：unsafe代码与并发正确性

Rust的类型系统很强，但强到一定程度也会“束手束脚”——某些追求极致性能的写法，类型检查器无法证明其安全性，Rust因此专门开了一个口子，允许开发者显式标注unsafe代码块。这类代码依然必须遵守Rust对安全代码的所有约束，只是编译器不再替你机械检查，安全与否全靠开发者自己把关。

Verus在这里能帮上大忙：它可以为unsafe代码块提供数学层面的安全性证明，相当于把编译器放弃掉的机器检查能力，重新“找补”了回来。

并发场景是另一块难啃的骨头。Rust本身以“无畏并发”著称，类型系统会拦截掉很多其他语言在并发编程中常见的低级错误。Verus在这个基础上更进一步，让开发者不仅能证明并发代码是安全的，还能证明它在逻辑上是正确的。

一个典型场景是锁（lock）。并发执行往往需要锁来保证某个处理器线程独占访问一份共享数据。Verus允许开发者给锁附加一个“不变式”（invariant）：任何人获得这把锁时拿到的数据一定满足这个不变式（比如某个数值永远是偶数），而在释放锁之前，必须证明数据依然满足这个不变式。更进一步，Verus还支持证明锁实现本身的正确性——这一点对Nitro隔离引擎这类依赖复杂自定义锁机制来换取高性能的系统尤其关键。

当然，任何验证工具的保证都不是凭空产生的，Verus也不例外。它的正确性最终依赖于几个层面：Verus工具本身是否可靠、开发者写的顶层规约是否真的表达了预期行为、对底层运行时（比如Rust标准库）所做的假设是否成立，以及把源码编译成可执行程序的整条工具链是否可信。这条“信任链”可以用下图简单表示：

亚马逊也提到，会在后续文章中详细介绍如何针对性地提升对这几个环节的信心，这也算是给读者提前挖了个坑。

走出亚马逊：Verus在开源生态里的样子

除了在亚马逊内部落地，Verus也已经被不少开源项目拿去证明各自的关键属性：

  • Vest：输入一份二进制数据格式的描述，自动生成对应的Rust解析/序列化代码，并附带Verus证明的正确性与安全性保证；
  • Verdict：面向x.509公钥证书标准的证书校验库，支持用户自定义校验策略，且正确性和安全性都经过证明；
  • CapybaraKV：验证持久化内存日志的正确性与崩溃安全性，确保系统意外断电或崩溃后数据依然处于良好状态；
  • Atmosphere：一个用Rust开发、并用Verus验证正确性的微内核（体积极小的操作系统内核）；
  • Anvil：证明Kubernetes控制器的正确性和“活性”（liveness），说明在合理假设下，控制器最终一定能把系统带回稳定状态；
  • CortenMM：一套包含可扩展锁协议的事务式内存管理系统，其并发代码的正确性由Verus验证。

Verus本身是一个完全免费、开源的项目，由学术界和产业界的一批研究者共同维护和推进。

小结：形式化验证会成为Rust开发的标配吗

从这篇文章能看出一个清晰的趋势：随着Rust在关键基础设施里的渗透越来越深，“类型安全”这一层保障正在变得不够用了。

亚马逊选择Verus的逻辑其实很朴素——规约和证明写在Rust源码里，语法贴近Rust，报错也是Rust风格，秒级反馈支持交互式开发，还能顺带啃下unsafe代码和并发这两块最难啃的骨头。这套组合拳,一方面照顾了人类开发者的学习成本，另一方面也天然适配了AI辅助编程的工作方式。

对于普通Rust开发者来说，短期内不一定人人都要给自己的代码写形式化证明，但了解Verus这类工具的存在和思路，至少提供了一种新的判断标准：什么样的代码值得投入成本去做“数学级别”的正确性保证——答案往往是那些一旦出错代价极高的关键路径，比如虚拟机隔离、密钥管理、支付链路这类系统。

参考资料

还在为写 Agent 框架频频死循环、上下文爆炸而束手无策？我的新专栏 《从0 开始构建 Agent Harness》 将带你：

  • 抛弃臃肿框架，回归“驾驭工程 (Harness Engineering)”的第一性原理
  • 用 Go 语言手写 ReAct 循环、并发拦截与上下文压缩引擎等，复刻极简OpenClaw
  • 构建坚不可摧的 Safety Middleware 与飞书人工审批防线
  • 在底层实现 Token 成本审计、链路追踪与自动化跑分评估
  • 从“调包侠”进化为掌控大模型边界的“AI 操作系统架构师”

扫描下方二维码，开启从 0 开始构建Agent Harness 的实战之旅。

还在为“复制粘贴喂AI”而烦恼？我的新专栏 《AI原生开发工作流实战》 将带你：

  • 告别低效，重塑开发范式
  • 驾驭AI Agent(Claude Code)，实现工作流自动化
  • 从“AI使用者”进化为规范驱动开发的“工作流指挥家”

扫描下方二维码，开启你的AI原生开发之旅。

商务合作方式：撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求，请扫描下方公众号二维码，与我私信联系。