用 PDD Kit 形式化验证智能体编写的全栈 Web 应用

Microsoft Research 2026-11-06T15:33:43.033434

概览

把形式化方法用在日常软件里。 PDD Kit 帮你把意图变成一份形式化规格，然后证明智能体写的代码对任意输入都满足这份规格；证明覆盖不到的地方，再用测试补上。它把形式化方法从少数专家的小众工作，带给了没有形式化方法背景的工程师，也带给了日常应用——就像这里展示的这个全栈 Web 应用。

随着 AI 智能体生成的代码越来越多，逐行人工审阅已经很难规模化。计划本该是你和编程智能体之间的契约，但实际上没有什么能强制智能体遵守它。智能体自己写的测试，通常检验的是它造出来的东西，而不是你要求的东西。PDD Kit 让智能体守住计划：它和你一起把意图写成 Verus 形式化规格，证明智能体的代码对任意输入都满足这份规格，证明覆盖不到的地方则回退到测试。

我们拿一个全栈 Web 应用试了试。在 GitHub Next 的 Chopin 里，我们用 PDD Kit 对 Pet Store（一个 Rust 写的商店应用）的登录逻辑做了形式化验证。Verus 加固了代码，还挖出了原本就存在的 bug，并证明了相较于规格，登录逻辑不存在 bug。开发者审阅了意图，全程没有逐行读过生成的代码。

计划是智能体应当遵守的约定，但没有任何机制强制它真的遵守。如今，编程智能体一次交付就可能写完整个功能，代码动辄几万行甚至几十万行。于是，逐行阅读 pull request 这种审查方式，已经跟不上这种新的工作节奏了。

现在大多数团队把精力放在计划和测试上：先告诉智能体想要什么，来回沟通直到计划和拟定的测试都合适，再交给智能体去实现。这份计划，也就是自然语言写的规格说明，本应是智能体必须遵守的约定。但实际上，智能体执行时会偏离它：它实现的跟你要求的有细微不同，然后为它自己的实现写测试，这些测试能通过，但测的不是你真正想让它写的代码。持续集成（CI）里测试数量越来越多、质量却参差不齐，测试覆盖率看起来还不错，而「你要求的东西」与「实际交付的东西」之间的差距，直到有人报 bug 或撞上一个棘手的边界情况才暴露出来。

那么，既然智能体生成的代码越来越多，怎样才能可靠地扩展审查？智能体写的代码通常有两种错误，细心的审查者一般能发现：漏掉了明显必需的东西，或者做了明显错误的事。光靠测试补不上这个缺口，因为测试只覆盖了程序能走的极一小部分路径。要补上它，需要另一种机制——这正是「证明」的用武之地。

审查问的是「这看起来对吗？」证明回答的是「这确实对吗？」数学证明能说明代码对每一个输入都满足其规格，包括测试套件可能漏掉的那些输入。对于已经明确规定下来的性质，这比单靠测试能提供更强的保证，尤其当逐行审查不现实的时候。

过去，形式化证明对日常软件来说成本太高：需要专家、需要学习陌生的语言、证明的体量往往是代码的许多倍，开发一套证明要花上几年。但如今有两点变了。第一，编码智能体的进步让它们越来越能在定义清晰的规格（spec）基础上帮忙生成形式化证明；第二，智能体也更能帮你写出形式化的规格。我们把这种新的软件开发范式叫做“证明驱动开发”（Proof-Driven Development，PDD）。PDD Kit 就是我们为它准备的工具包。

PDD Kit 怎么工作

粗略地说，PDD Kit 之于形式化方法，就像 Spec Kit 之于规格驱动开发。它以伙伴的形式运行在 Chopin 里——这是 GitHub Next 打造的实时多人协作规划环境，团队和智能体可以在同一份共享文档里一起做规划。整个工作流分成两半（图 1）。前半段由团队成员用自然语言审阅意图。PDD Kit 会像一位细心的评审人那样提出问题，边问边解释相关代码，并把答案记录到“意图文档”（intent artifact）里——这份文档负责把用户意图和形式化规格或测试衔接起来。用户意图中能够形式化的部分，会被转成形式化规格；剩下的部分只能靠信任接受，则转成非形式化规格，用于生成测试。PDD Kit 会自动生成证明，说明代码满足推导出的形式化规格；同时为那些非形式化规格生成高质量的测试。整个过程你都不需要具备形式化方法的背景。

图 1. 用 PDD Kit 进行证明驱动开发。团队成员敲定意图，Verus 和测试套件负责让代码符合意图。

因此，PDD Kit 里的每一项结果都会说明它建立在哪一类验证之上：

形式化验证是用数学证明来说明：对于所有可能的输入，代码都满足它的规格。执行这项检查的工具叫做验证器（verifier）。目前 PDD Kit 使用的验证器是 Verus——一种面向 Rust 的证明语言，由微软研究院、卡内基梅隆大学、VMware Research、苏黎世联邦理工学院、MPI-SWS、新南威尔士大学悉尼分校、得克萨斯大学奥斯汀分校、密歇根大学、不列颠哥伦比亚大学、威斯康星大学麦迪逊分校和魏茨曼科学研究所共同开发。

经验性验证靠运行代码、观察行为来检查。它能覆盖证明触及不到的地方，比如第三方加密库或用户界面。具体手段包括单元测试、端到端测试、终端自动化、浏览器 Agent，以及浏览器无法驱动时使用的 computer-use Agent。测试通过只能说明代码在试过的那些输入上能跑通，所以 PDD Kit 把它标记为「证据」而非「证明」。

两者的分界线就是可信计算基（TCB）：证明所假定「按描述行事」的那部分代码。PDD Kit 把这条界线明确摆出来，并要求你对每一块逐一确认。

压轴大戏：一个全栈 Web 应用

为了展示 PDD Kit 能与现有代码库配合，我们做了 Pet Store——一个完全用 Rust 写的全栈 Web 应用。后端用 Axum 和 SQLite，负责库存、促销、订单和结账。店面是用 Leptos 编译成 WebAssembly 的前端。加起来大约 5,000 行 Rust。为控制篇幅，本文只聚焦登录逻辑的形式化验证，但同样的流程可以用于验证整个应用的功能正确性。PDD Kit 建议从应用最敏感的部分入手，逐步推进验证。登录漏洞可能把客户的账号甚至管理员权限拱手交给攻击者，所以这里最值得优先投入证明工作。

开发者在 Chopin 里提的整个需求只有两句话：验证 backend/src/handlers/auth.rs 里的登录逻辑。以下是我的需求：

只有当提交的凭据与某个已存在且处于激活状态的账号所存储的凭据匹配时，登录请求才算成功。
登录失败时，不得泄露用户名是否存在。
每一次失败的尝试都必须被记录下来，以便限流机制据此采取行动。
登录成功后必须返回一个会话令牌，且该令牌只绑定到通过认证的那个用户，不能绑定到任何其他人。

从两句话到一份规范

拿到这四条需求后，PDD Kit 像一位仔细的评审者那样开始追问：什么算「活跃」？查用户名之前要不要先规范化？如果要，由谁来做？会话能不能在改密码之后继续有效？登录过程中数据库报错，应该怎么处理？每个答案都会被写进意图文档（intent artifact）——它夹在开发者用大白话表达的意图和检查代码的产物之间。

接着，这份文档把意图拆成两半。Verus 能推理的部分，变成形式化规范，比如登录处理器的控制流、在什么条件下发放会话、返回的 token 和已认证用户之间的关系。无法证明的部分则变成非形式化规范，靠测试兜底——因为这些代码只能被信任，不能被证明。具体包括：Argon2 能正确校验哈希、SQLite 驱动返回查询所要的行、Axum 提取器按文档填充请求。

证明发现了什么

把规范变成证明的过程，逼着 agent 把发放会话的每一个条件都明确写出来。现有 bug 就是在这里暴露的：有的代码路径在出错时仍然返回会话；有的在用户名查找的某个分支跳过了检查，另一个分支却做了检查。现有测试套件一个都没抓到，因为测试跑的是实现碰巧有的路径，而不是意图要求的路径。

修复之后，Verus 证明了该处理器对所有输入都满足规范，而不只是测试碰巧试过的那几个输入。这正是文章反复强调的区别：测试是证据，证明是保证。

明确可信计算基

PDD Kit 把可信计算基（Trusted Computing Base）显式地列出来，而不是让它隐含在背景里。证明过程假定密码哈希库、数据库驱动、HTTP 框架和会话存储的行为与描述一致，因此这些假设逐条列出，供人确认。每一步都能看清「已证明」和「已测试」的边界，每个结果都会说明它依赖的是哪种验证。

开发者实际审查了什么

开发者审查的是意图工件：需求、审查者提出的问题、对应的回答，以及可信假设清单。他们没有逐行阅读生成的 Rust 代码。原本发生在拉取请求（PR）阶段的审查，被提前到了契约（contract）阶段，而契约随后由验证器来保证，而不是靠人的注意力来保证。

要点

PDD Kit 并不要求你更信任智能体。它要求你明确说出自己要什么，然后让智能体证明它确实做到了。对于应用中敏感的部分——身份认证、授权、资金、访问控制——把审查精力花在这上面，比逐行读一份没人有时间读的 diff 更划算。

从应用里你最不希望出错的那部分开始，写下它必须做到什么，然后让证明来约束代码。

s: 只有密码正确才能拿到令牌。只有管理员账户才能拿到管理员令牌。

我们故意让请求保持粗糙。捕捉用户意图、把用户请求转成证明可以检查的东西，是 PDD Kit 的工作。

第 1 步：先提问，再写代码

PDD Kit 的规划工作流 pdd-plan 会读取代码，然后在写任何东西之前，先在「决策」标签页里带着问题回来。当某个问题取决于代码如何运作时，卡片会先解释那部分：目标是什么、各组件如何配合、涉及哪个具体函数，这样你不用打开源码就能回答。

图 2。第一张决策卡。光写「只有密码正确才行」，一个拒绝所有人登录的实现也能满足它。把两个方向都证明一遍，才能排除这种情况。

这个问题看着吹毛求疵，但很关键。"只有密码正确才发 token"排除了坏情况——密码错误却拿到 token；而一个拒绝所有人的登录逻辑同样完全满足这个承诺。"密码正确时一定能拿到 token"正好排除了这种情况。形式化地说，前者是一个蕴涵（token ⇒ 密码正确），后者是它的逆命题。合在一起才是"当且仅当"。如果放任 agent 自己决定，它只会悄悄选一种，不会告诉你；但这里开发者两种都选了。

第二步：一份人可读的意图地图

对话进行中，PDD Kit 会在计划顶部维护一个粗略的工作区，让用户不必翻回长长的聊天记录去找之前达成的共识。里面包括正在规格化的登录流程图、标明哪些要证明、哪些要信任的规格全景图，以及在图更有帮助时给出的心智模型。针对登录，PDD Kit 画了一个售票台（图 3）。

图 3. PDD Kit 为登录构建的心智模型。你递进的字段决定窗口，窗口决定柜台，柜台决定角色，密码不对什么都不会打印。

在它下方，意图地图把每条需求都追溯到开发者自己的原话，并记录它是怎么定下来的（图 4）。每条记录都链接到形式化规格中建模它的那一节，以及覆盖它的测试；规格那一节会展示 Verus 合约的片段，并加上注释，让开发者能看到形式化规格是如何建模自己的意图的。

图 4. 决策之后的意图地图条目：登录只有在使用了该账号的正确密码时才发 token，且只要密码正确就一定会发。

流程图展示了密码校验所有可能的结局。图 2 中的决策卡片，正是 agent 否则会悄悄替你做主的那种歧义。图 5 展示了这种差别在纸面上有多小：两种读法只在一个格子上不一致——密码正确却没拿到 token。

图 5. 同一句话的两种读法。它们只差一个格子，而那个格子决定了证明必须建立什么。

第 3 步：证明登录函数

在动手搭建之前，PDD Kit 会先请团队整体批准计划。它的初稿只证明了登录的核心决策——选表、对密码做校验——而把围绕它的 handler 当作可信代码，并保持对它的测试。这是一个合理的默认做法，也是 PDD Kit 推荐的方式，但这位开发者想要更多。handler 是查询被 await、token 被签名的地方，而这段“胶水”代码恰恰是重构时可能悄悄调换两行的地方。

所以在意图评审时，开发者选择给登录 handler 单独写一份异步规范，让证明也覆盖这段胶水代码，而不是直接信任它（图 6）。

图 6. 证明登录的更多部分，意味着要信任更多小包装。卡片在开发者做出选择之前就说明了这一点。

这个选择把几乎所有东西都纳入了证明，登录 handler 只剩解包请求这一件事。一个新的异步函数 login_flow 把契约从请求字段一路带到 token 或 HTTP 错误。

随后 PDD Kit 把修订后的计划拿回来重新签字确认，因为“匹配意图”不等于“证明”，它也不会批准新增的信任或更大的范围。

第 4 步：证明在哪里停下

关于一个程序，有很多东西你没法证明，而登录几乎把这些都碰上了：

验证器看不到的代码。 bcrypt 的哈希、sqlx 的查询、jsonwebtoken 的签名，都在别的 crate 里，位于证明范围之外。
关于外部世界的事实。 SQLite 此刻存了什么、时钟此刻显示几点，是程序的输入，而不是程序代码能确立的东西。
事情是否完成、以及完成得多快。 规范说的是登录给出回答时你会得到什么。查询卡住，或者查询很慢，在规范里都不算破坏。
任何需要人来判断的东西，比如错误信息是否有帮助、界面是否说得通。
没人写下来的东西。 证明只覆盖它的规范，对规范之外的需求一无所知。

这正是经验性验证的用武之地。PDD Kit 明确划出了可信边界，也就是这条证明所依赖的那部分 TCB（可信计算基）。它把每个可信组件包进一个小函数里，并为该函数设定一个假定的契约，用的是 Verus 的 #[verifier::external_body] 或 external_fn_specification；它请开发者逐个确认这些假定，并把每个假定条款对应的测试写进计划。

就登录功能而言，开发者确认了六个部分：

两个查询：Customer::find_by_email 和 Admin::find_by_username。每次成功的异步查询返回的，恰好是它自己那张表里对应这个 email 或用户名的那一行，或者返回空。
check_password，是包在 bcrypt::verify 外面的一层薄封装。只有当存储的哈希无法被 bcrypt 读取时才报错；返回 Ok(true) 就意味着密码完全正确。
generate_token，用配置的密钥对给定的声明（claims）原样签名；签名失败时报 500。
expiry_from_now，读取当前时钟，写入的过期时间恰好是 24 小时之后。
database_error，把查询失败转成当前的 500 响应，带上 sqlx 的错误信息。
登录 handler 的外壳，拆解请求，把字段原样传给 login_flow。

在规范里，查询函数的代码留在原处，通过 external_fn_specification 从外部获得契约：

/// Looks up a customer by exact email.
/// Trusted, not proved: the SQL query runs in sqlx, which Verus cannot check.
/// Every customer promise of `login_flow` rests on it.
#[verifier::external_fn_specification]
pub async fn ex_customer_find_by_email(pool: &sqlx::SqlitePool, email: &str) -> (r: Result<Customer, sqlx::Error>)
    ensures
        // When the query succeeds, it returns the customers row on
        // file for exactly this email, or None when there is none.
        r matches Ok(found) ==> found == customer_on_file(email@),
{
    Customer::find_by_email(pool, email).await
}

时钟则是一个标记了 #[verifier::external_body] 的小封装。Verus 只使用它的 ensures 子句，从不读取函数体：

/// 读取时钟并计算令牌 24 小时后的过期时间。
/// 此函数受信任但未经证明：chrono 的时钟不在证明范围内。
/// 如果时间超出范围，它会 panic，就像今天的登录逻辑一样；
/// 这个 panic 并不在承诺范围内。
#[verifier::external_body]
pub fn expiry_from_now()

    -> (r: Expiry) ensures
        // 过期时间恰好是读取时钟后的 24 小时（86,400 秒）。
        r.exp as int == r.now as int + 86_400,
    { ... }

图 7 把这三层放在一起展示：Verus 证明了什么、人们接受并由测试检查什么，以及没有任何人承诺什么。

图 7. 登录证明的终点在哪里。Verus 对任意输入都证明核心逻辑。人们接受信任环，并由测试检查。计划列出了无人承诺的内容。

图 8 梳理了哪些内容会被证明、哪些会被信任。每个信任决策都是单独一张卡片，展示 Verus 会凭信任接受的子句、开发者接受了什么、以及如果假设错误会导致哪个承诺失效（图 9）。每个被假设的子句随后都会在计划的“经验验证”部分获得实际检查，以 Given/When/Then 场景的形式写出来，而且这些场景会在任何测试存在之前完成（图 10）。条目在运行前标注为“已计划”，运行后则记录命令结果和对应的提交。

图 8. 登录中哪些被证明、哪些被信任。绿色函数由 Verus 对任意输入证明。琥珀色部分受信任，由开发者接受，并由计划 §4.1 中计划的测试检查。

图 9. check_password 的信任卡片。Verus 凭信任接受这两条子句，因此由人来接受，并由两个测试检查。

图 10. 针对受信任的 check_password 的计划测试，在测试存在之前就写好。计划把通过的测试标记为证据，而非证明。

计划也同样明确列出了没有任何人承诺的内容：登录 future 一定会完成、超出范围的时钟不会 panic、任何关于尝试时序或速率的内容，以及其他端点如何读取角色。

第 5 步：阅读规范

团队审阅的是意图工件（intent artifact）。它是 PDD Kit 用 Verus 合约写成的形式化规范的白话版本。你可能会想，现在是不是得有人去读证明，而不是读代码了？其实不需要，因为证明由编码智能体来写，而 Verus 会检查证明的每一步。只要 Verus 接受了证明，它就是成立的，不管有没有人读过。规范才是证明必须满足的标准，所以人们真正审阅的是规范。这份规范很短，几分钟就能学会怎么读。

每个函数都有一个 ensures 块：里面写的是关于其结果 r 的陈述，这些陈述对任何可能的输入都必须成立。构建时 Verus 会检查它们；只要有任何一条子句哪怕对某一个输入可能不成立，构建就会失败，Verus 会指向那条子句。每条子句读起来都是一个 if-then。图 11 拆解了对应开发者第一条需求的那条子句。

图 11. 针对“只有密码正确才能拿到令牌”这一需求，login_flow 上的 ensures 子句。同一个账户 a 出现在每一行，把密码检查和令牌绑定在一起。注意同一个 a 出现在每一行，这让密码检查和令牌关联起来。

举个例子，设想有这么一个 bug：登录时用某个账户校验密码，却给另一个账户签发令牌。Bob 用自己的正确密码登录，拿回来的却是 Alice 的令牌。

    role@ == a.role),

// The right password for the named account always gets a
// token, unless a lookup or signing failure gives 500.
(named_account(email, username) matches Some(a) && password_matches(password@, a.password_hash))
    ==> (r is Ok || r matches Err(AppError::Internal(_))),

// A login naming an account nobody holds gets
// 401, unless the lookup fails with 500.
((email is Some || username is Some) && named_account(email, username) is None)
    ==> (r matches Err(AppError::Unauthorized) || r matches Err(AppError::Internal(_))),

// A wrong password for an account whose hash bcrypt
// can read gets 401, unless the lookup fails with 500.
(named_account(email, username) matches Some(a) && bcrypt_verdict(password@, a.password_hash) == Some(false))
    ==> (r matches Err(AppError::Unauthorized) || r matches Err(AppError::Internal(_))),

// An account whose stored hash bcrypt cannot read gets 500 and no token.
(named_account(email, username) matches Some(a) && bcrypt_verdict(password@, a.password_hash) is None)
    ==> r matches Err(AppError::Internal(_)),

// The admin role only for an admins row
// found by username, with no email sent.
(r matches Ok(t) && token_claims(t@, config.jwt_secret@) matches Some(c) && c.role@ == admin_role())
    ==> (email is None && username matches Some(u) && admin_on_file(u@) is Some),

// An email login's token always carries the customer role.
(r matches Ok(t) && email is Some)
    ==> (token_claims(t@, config.jwt_secret@) matches Some(c) && c.role@ == customer_role()),
{ unimplemented!() }

信任边界在代码里也能看到。check_password 是 Verus 不检查函数体的函数之一。它的合约把这个函数和 bcrypt_verdict 绑在一起，而 bcrypt_verdict 是 bcrypt 的一个未解释模型，没有任何公理：

/// 询问 bcrypt：`password` 是否匹配存储的 `hash`。
/// 可信但未证明：Verus 无法检查 bcrypt 的哈希过程，
/// 因此这个包装函数的合约是假设成立的。
/// `login_flow` 的每一个密码承诺都依赖它。
#[verifier::external_body]
pub fn check_password(password: &str, hash: &str) -> (r: Result<bool, String>)
    ensures
        // 当且仅当 bcrypt 能读取存储的哈希时，它才返回 Ok。
        r is Ok <==> bcrypt_verdict(password@, hash@) is Some,
        // 它的返回就是它的判定：密码正确返回 true，
        // 其他任何密码返回 false。
        r matches Ok(b) ==> bcrypt_verdict(password@, hash@) == Some(b),
{
    bcrypt::verify(password, hash).map_err(|e| e.to_string())
}

上面的文档注释说明了有哪些东西依赖它：login_flow 的每一个密码承诺。每次登录最终都会落在少数几个出口之一，其中只有一个出口会拿到 token（图 13）。证明一次性覆盖了所有这些出口。

图 13. 从计划看，一次登录所有可能的结束方式。

login_flow 是异步的：它会等待一个数据库查询。Verus 可以给异步函数加合约，但有一条规则值得知道（图 14）：requires 在调用创建 future 时检查；ensures 描述你 await 它时拿到的值。没有任何东西保证这个 future 一定会完成，所以查询卡住也不会违反任何条款。login_flow 的文档注释就是这么明说的：

/// ... 不保证 future 会完成。
pub async fn login_flow(...) -> (r: Result<LoginResponse, AppError>)

图 14. 对于同步 fn 和异步 fn，合约分别在什么时候被检查。

login_flow 之所以能保持简短，是因为它由更小的、已经证明过的组件拼成。lookup_target 负责选表。login_core 等待查找结果，再调用密码校验关 decide_login。issue_token 签发令牌，或者把拒绝映射成对应的 HTTP 错误。每个组件都有自己的契约。Verus 只依据这些契约来证明 login_flow，不需要重新阅读各组件的实现体。如果改动 decide_login 的实现体，就只需要重新证明 decide_login 本身。下面是最小的那个组件，完整列出，再加上密码校验关的开头和结尾：

pub fn lookup_target(email: Option<String>, username: Option<String>) -> (r: Result<LookupTarget, LoginError>)
    ensures
        // 一旦提供了邮箱，就以邮箱为准：按该邮箱精确查找客户。
        email matches Some(e) ==> r == Ok::<LookupTarget, LoginError>(LookupTarget::CustomerByEmail(e)),
        // 没有邮箱时，用用户名把查找指向管理员表，按该用户名精确查找。
        email is None && username matches Some(u) ==> r == Ok::<LookupTarget, LoginError>(LookupTarget::AdminByUsername(u)),
        // 两者都没有，就以缺少身份信息为由拒绝登录。
        email is None && username is None ==> r == Err::<LookupTarget, LoginError>(LoginError::MissingIdentity),

pub fn decide_login(target: &LookupTarget, found: Option<Customer>, password: &str) -> (r: Result<Claims, LoginError>)
    ensures
        // 没查到记录：按 Unauthorized 拒绝，
        // 和密码错误给出同样的答复。
        found is None ==> r == Err::<Claims, LoginError>(LoginError::Unauthorized),
        // 只有查到记录、且存储的哈希与密码匹配时，才返回 Claims。
        r is Ok ==> found is Some && password_matches(password@, found->Some_0.password_hash@),
        // 查到记录且密码正确，就一定会拿到 Claims。
        found matches Some(a) && password_matches(password@, a.password_hash@) ==> r is Ok,
        ...
        // 查管理员表时，角色文本为 "admin"。
        r matches Ok(c) && target is AdminByUsername ==> c.role@ == admin_role(),
        // 查客户表时，角色文本为 "customer"。
        r matches Ok(c) && target is CustomerByEmail ==> c.role@ == customer_role(),

login.rs 概览

图 15 展示了整个规范文件 verified/src/login.rs 的结构。从上到下分为四层：头信息、Verus 需要了解的导入和类型、对外部世界的抽象视图、将该视图连接到真实代码的可信契约，以及证明必须满足的五条契约。

图 15. login.rs 的各个部分，按文件顺序排列。灰色是头信息和类型，紫色是仅出现在契约中的数学定义，琥珀色是可信部分，绿色是已证明部分。

以下是其中两个不太直观的部分（有删节）。external_type_specification 引入一个 Verus 未定义的类型。连接池保持不透明，而 customers 行则保留字段可见：

/// 连接池，对证明不透明：只有查找操作的契约
/// 说明它返回什么。
#[verifier::external_type_specification]
#[verifier::external_body]
#[verifier::reject_recursive_types(DB)]
pub struct ExPool(sqlx::Pool<DB>);
...
/// customers 行，其字段对证明可见。
#[verifier::external_type_specification]
pub struct ExCustomer(Customer);

而 LoginError 将决策与 HTTP 响应分开，这正是 issue_token 能将每种拒绝对应到当前状态码的原因：

/// 登录未能获得令牌的原因。
pub enum LoginError {
    /// 既未发送邮箱也未发送用户名：400 Bad Request。
    MissingIdentity,
    /// 账户不存在，或密码不匹配：401 Unauthorized。
    Unauthorized,
    /// bcrypt 无法读取存储的哈希值，附带其消息：500 Internal。
    UnreadableHash(String),
    /// 查找查询失败：500 Internal，附带 sqlx 的消息。
    Database(sqlx::Error),
}

在计划返回给你之前，两个审查代理会从意图工件中对推导出的形式化规范挑毛病，确保

第 6 步：证明、检查、填补缺口

翻译质量足够高，规范与你要求的一致，且不会承诺超出证明能力范围的东西。规范细化在后台运行，接受实时用户反馈，反复迭代直到审查者一致认为规范是可靠的。

开发者审到签署规格这一步就结束了。之后的事情——实现和证明——都交给机器检查，所以本文重点讲规格，而不是证明。开发者签字确认后，Build plan 阶段（图 16）会把批准后的计划交给 pdd-prove，由它转成一张小任务图（图 16）。以登录为例，一共七个任务：让 login.rs 在后端 crate 里能在 Verus 下编译，证明决策、令牌和整个流程，再为可信包装器和端到端登录写测试。

图 16. Build plan 把已批准的规格拆成开发机上的七个任务。

第一个任务要让 login.rs 在 Verus 下编译通过，同时不改变任何契约承诺；做不到就停下来问，而不是削弱契约。每个任务都走同一个循环：编码智能体写实现和证明，Verus 对照派生出的形式化规格进行检查。凡是落在可信边界内的部分，都要补上计划要求的测试。大语言模型（LLM）验证器会把计划、规格和结果放在一起对照，寻找缺口：哪些需求既没有证明，也没有通过的检查。发现缺口就打回给编码智能体，直到补完为止。如果规格本身有缺口，比如两条需求互相矛盾，就会作为待决问题退回给开发者。证明的质量不会超过规格的质量，所以 pdd-prove 也会检查规格。当模型自己写规格，或者被专门调教成产出证明时，它往往会落在很弱的不变式上：这些子句能通过验证，却几乎排除不了什么。它们确实证明了点什么，但很少是你真正关心的东西。我们把这称为“感觉式验证”（vibe verification）。这正是为什么确保你的意图与智能体对齐如此重要，也正是 PDD Kit 擅长解决的问题。这个循环严格禁止偷换目标。如果某个异步构造无法在固定版本的 Verus 中表达，任务就会停下来询问团队，而不是改用非异步辅助函数，或者削弱契约。

PDD Kit 如何消除某类 bug？

变异检查是 PDD Kit 防止“凭感觉验证”的手段。pdd-prove 会在代码的临时副本里，针对每条 ensures 子句植入一个 bug，比如拒绝所有人，或者先检查用户名再检查邮箱，然后 Verus 必须针对该子句拒绝每一个变异体。如果某个变异体通过了，说明那条子句什么也没约束住，它就会作为缺口被报回来。

第 7 步：对照已验证的代码审查意图

任务通过后，pdd-prove 会打开拉取请求。这些 PR 会新增一个 verified/ crate，里面包含 login_flow、它的各个组件、它们的证明，以及带测试的可信包装层，并把真正的登录处理器接到 login_flow 上，同时保留现有的 HTTP 状态码。你验证过的逻辑会接入并加固生产环境的登录路径，而不是它的一个副本。开发者无需逐行审查生成的代码就能合并。整个过程中，审查其实一直发生在意图产物上，团队在那里拥有最终决定权。我们把审查重心从代码审查更多地转向了意图审查。拉取请求相当于一张收据，它的描述把每条登录需求标记为“已形式验证”或“已经验检查”。合并，就是证明加入团队正常工作流的地方。PDD Kit 的 pdd-ship 工作流会把 Verus 检查加进 CI，和经验测试放在一起，这样以后无论谁——人还是 agent——对登录做任何改动，都必须继续针对同一份规格证明，证明一旦被破坏，构建就会像测试失败一样失败。而且因为证明覆盖了所有输入，PDD Kit 会裁掉那些只是在重复检查已被证明内容的测试，比如针对密码闸门的示例测试，保留那些守护可信边界的测试，于是 CI 同时变得更强、更精简。

证明说了什么，没说什么

“完全验证”很容易被过度吹嘘，所以我们明确一下这里到底在声称什么。

已证明。 login_flow、login_core、lookup_target、decide_login 和 issue_token 这几个函数的函数体，对任何输入都满足各自的契约。登录逻辑会选对表，拿请求里的密码去比对它所指定账户存储的哈希值，用该账户的 id 和它所在表赋予的角色签发 token；其余情况一律拒绝，返回现有的 400、401 或 500，并且不签发 token。

受信任且已测试。 两次数据库查询、基于 bcrypt 的 check_password、时钟、token 签名、数据库错误消息，以及处理函数对请求的解包，都落在证明范围之外，各自依赖一份开发者已经接受的假定契约。针对真实 bcrypt、真实 SQLite schema 和真实路由的测试覆盖了这些部分。

假定。 Verus、Rust 编译器和 Z3 工具链，以及 Verus 的标准库 vstd。

为什么选 Rust

PDD Kit 目前只验证 Rust，因为 Verus 只支持这门语言。如果你的代码库本来就是 Rust，那不用做任何迁移。其他语言的代码可以移植到 Rust，再用同一份规格检查；非 Rust 项目也可以通过绑定调用经过验证的 Rust 代码。还有一个不太明显的优势：一旦不再需要逐行通读代码来确认正确性，可读性就不再是选语言的主要理由。你可以为了速度和安全性挑一门语言，想优化到多狠就优化到多狠，因为任何破坏规格的改动都会让证明失败。

PDD Kit 能带来什么

PDD Kit 是一个研究原型，目前只能验证 Rust 代码，因为 Verus 只支持这门语言。其他语言的代码可以移植到 Rust，再对照同一份规格说明做检查；非 Rust 项目也可以通过绑定调用经过验证的 Rust 代码。写证明仍然很费功夫，主要成本在证明本身，而一份清晰的规格说明能把这份成本压下来——这也是 PDD Kit 把大量精力放在“先搞对意图”上的原因。我们会从出错代价最高的地方入手，比如登录、支付、权限，然后一块一块地验证代码库的其余部分。Pet Store 的登录只是其中一个应用的一个片段：一份谁都能读懂的规格说明，一个证明代码与规格相符的 Verus 证明，以及针对证明所依赖的每一项假设编写的测试。

我们想把最薄弱的环节说清楚。保证的强度取决于六个可信组件，其中两个承担了主要分量：check_password 支撑所有关于密码的承诺，两个查找支撑所有关于“令牌指向哪个账户”的承诺。测试为它们提供支持，但没有任何东西能证明它们。我们预计这个可信边界会随时间显著缩小，让越来越多代码进入形式化验证范围，我们也想知道这套方法能扩展到多大规模。我们真正改变的是人们审查的对象。团队不再主要依赖逐行审查智能体生成的代码，而是用平实的语言审查代码的意图，再由证明来确认实现与意图一致。

证明让代码对规格负责。计划本就该是契约，现在智能体必须真正守住它。

致谢

这项工作由 Microsoft Research Catalyst Lab、GitHub Next 和软件工程研究组（RiSE）合作完成。感谢 GitHub Next 的 Maggie Appleton 和 Krzysztof Cieślak 在 Chopin 项目上的合作，感谢 Nikhil Swamy、Lef Ioannidis、Janardhan Kulkarni 和 Shuvendu Lahiri 就形式化验证与意图形式化给出的反馈和讨论。也感谢 F*/Pulse 和 Verus 团队的支持。最后，感谢 GitHub Next 的 Idan Gazit 对本次合作的推动。

常见问题

如果规格是 AI 写的，谁来保证规格本身正确？如果规格错了，验证出来的代码不也是错的吗？

答案是你来保证，而且你说得对——规格错了，代码也会错。形式化证明只能证明代码满足规格，不能证明规格符合你的真实意图。正因如此，PDD Kit 的设计基于现有的“意图形式化”研究。pdd-plan 工作流会先阅读你的代码，在动笔之前向你提问，再把你的回答转化成一个 Verus 规格和一份通俗易懂的计划书，交给你审批——遇到含糊之处会主动标记出来，而不是自行猜测。两个审查代理（reviewer agent）会检查规格，pdd-prove 工作流则会在每条规格子句上植入一个 bug，用来揪出那些“能通过验证、但实际上什么都没约束住”的子句。当然，错误的规格仍然可能出现。所以 PDD Kit 强调把需求写明确、找出歧义点，并让开发者在验证开始之前始终参与规格的审查和批准。

这和规格驱动开发（SDD）、测试驱动开发（TDD），或者干脆让代理自己检查自己的代码，有什么区别？

区别在于：是什么在约束代码符合计划。

方法	谁在检查代码
规格驱动开发（SDD）	没有任何机制强制执行规格
测试驱动开发（TDD）	在部分输入样本上跑测试，而且测试往往是照着已写好的代码来写的
代理自检	还是写代码的那个模型
证明驱动开发（PDD）	Verus 自动验证“代码满足规格”的形式化证明

你批准过的 PDD 沿用了 SDD 的规划循环，在形式化证明覆盖不到的地方仍然会使用测试。测试只能检查部分输入，而形式化证明则能在其形式模型覆盖的所有输入上、在声明的假设前提下，确立代码满足指定的性质。

证明到底是什么？在哪里运行？结果是确定的，还是又交给一个语言模型（LM）？要跑多久？

证明本身就是一段 Rust 代码，里面嵌入了 Verus 的语法结构，由 Verus 调用 Z3 求解器做机械检查。它跟着你的 Rust 构建走：pdd-prove 工作流在证明阶段运行它，pdd-ship 工作流则把它加进构建和 CI，证明一旦不过，构建就失败。这个检查是确定性的，不涉及任何模型。模型负责写规格、写代码、写证明，但最终判定通过与否的，只有那次确定性的 Verus 运行。检查耗时取决于代码规模和证明难度：小模块通常几秒，大一些的代码库可能要几分钟。

如果验证取代了逐行代码评审，那我到底还要评审什么？

PDD Kit 把评审的重心更多移到「代码应该做什么」上，再用形式化验证额外保证实现确实满足这些要求。开发者需要评审的，是自然语言写的计划、形式化规格，以及那些不在证明覆盖范围内的可信组件。最终的拉取请求（PR）会说明哪些部分经过了形式化验证、哪些经过了测试、哪里可能还需要人工把关。在 Pet Store 这个全栈 Web 应用上，这套做法减少了对生成代码逐行详审的依赖。

只支持 Rust 吗？为什么选 Verus，而不是别的验证工具或形式化语言？

选 Verus，是因为它能直接验证 Rust 代码，这和 PDD Kit 的目标一致——把形式化验证融入现有的 Rust 开发流程。其他证明语言（比如 Lean、F*、Rocq）走的是不同的形式化验证路线，各有取舍。PDD Kit 背后的技术思路，同样可以帮助它们发挥作用。

AI 智能体生成代码的规模，人类很难逐行审查。PDD Kit 的做法是：先把开发者的意图写成形式化规格（用数学方式精确描述代码应该做什么），再让 AI 生成的代码接受这些规格的检验，确保代码确实按开发者的意图工作。它会把开发者意图转换成 Verus 规格；针对每一个输入，证明 AI 生成的代码都满足该规格；在证明不太现实的地方，则改用测试来验证。这样一来，开发者只需要审查意图，不用逐行检查代码。

查看原文