> ## Content Index
> Fetch the complete content index at: https://www.hubwiz.com/blog/llms.txt
> Use this file to discover other available public pages before exploring further.

# AI 写的代码不用逐行读：微软 PDD Kit 用证明替代评审
- URL: https://www.hubwiz.com/blog/pdd-kit-formal-verification-agent-written-apps/
- Published: 2026-11-07T09:26:30.000Z
- Updated: 2026-11-07T09:56:15.000Z
- Description: 计划本该是 agent 必须遵守的契约，却没什么强制它遵守。PDD Kit 先把意图谈成可读规格，再让机器证明代码对每个输入都满足它，证不到的地方退回测试。
- Author: admin
- Tags: AI 编程, 形式化验证, 代码评审, Rust

**agent 现在能一次交付一整个功能，动辄几万到几十万行代码。逐行读 PR 这件事，已经跟不上这种工作方式。**

现在多数团队把投入放在计划与测试上：告诉 agent 你要什么，来回几轮把计划和提议的测试磨对，然后交给 agent 实现。这份计划——或者自然语言规格——本该是 agent 必须遵守的契约。但实践中，agent 会偏离它：它实现了稍微不一样的东西，然后为**自己的实现**写测试让它们通过，而不是为你想要的代码写测试。CI 因为大量低质量、数量众多的测试而膨胀，覆盖率看起来健康，而"你要的"和"上线的"之间的差距一直藏着，直到一份 bug 报告或一个恶劣的边界情况出现。

那怎么在 agent 生成越来越多代码的同时，可靠地把评审规模化？

agent 写的代码会以两种方式出错，而一个仔细的评审者通常能抓住这两种：**它漏掉了某个明显必需的东西，或者它做了某个明显错误的事。** 光靠测试补不上这道缝，因为测试只覆盖程序可能行为中极小的一片。要补上它，需要另一种机器——这就是证明的用处。

评审问的是"这看起来对吗？"，证明回答的是"这是对的吗？"。一个数学证明表明：代码对**每一个**输入都满足其规格，包括你的测试集漏掉的那些。对于被规格化的性质，这比单靠测试提供更强的保证，尤其在逐行评审已不现实的时候。

证明过去对日常软件来说太贵了：要专家、要用陌生的语言、证明比代码大好几倍、开发要几年。但从那以后有两件事变了。第一，编码 agent 的进展让"从良定义的规格生成形式证明"越来越可行。第二，agent 现在也更能帮你写形式规格。我们把这个新的软件开发范式叫**证明驱动的开发（Proof-Driven Development，PDD）**，PDD Kit 就是它的工具箱。

![PDD Kit hero](https://www.hubwiz.com/blog/content/images/2026/11/img_9cec1be357dfbc359111bd5076ca0035-800.jpg)

## 速览

- **把形式方法带进日常软件。** PDD Kit 帮你把意图变成形式规格，然后证明 agent 写的代码对每个输入都满足它；证明到不了的地方，用测试补。
- **逐行人工评审难以规模化。** 计划本该是你与编码 agent 之间的契约，但没有任何东西强制 agent 遵守它。agent 写的测试通常检查的是"它建了什么"，而不是"你要了什么"。
- **PDD Kit 让 agent 守住计划。** 它和你一起把意图变成 Verus 形式规格，证明 agent 的代码对每个输入满足该规格，并在证不到的地方退回测试。
- **我们在一款全栈 Web 应用上试了。** 在 GitHub Next 的 Chopin 里，我们用 PDD Kit 形式化验证了 Pet Store（一个 Rust 商店）的登录逻辑。Verus 加固了代码并暴露出既有 bug，证明了"相对于规格，登录不存在 bug"。开发者只评审了意图，从未逐行读生成的代码。

![PDD 流程图](https://www.hubwiz.com/blog/content/images/2026/11/img_99c700a04028cf47a95923b0690f8e31-800.jpg)

*图 1：用 PDD Kit 做证明驱动的开发。团队把意图谈定，Verus 与测试集让代码守住它。*

## PDD Kit 怎么工作

PDD Kit 之于形式方法，大致相当于 Spec Kit 之于规格驱动开发。它作为 Chopin（GitHub Next 的实时多人规划环境）里的一个伙伴运行——团队与 agent 在同一份共享文档里规划。

工作流分两半（图 1）。第一半，团队成员用自然语言评审意图。PDD Kit 会问一个仔细的评审者会问的问题，边问边解释相关代码，并把答案记录进"意图工件（intent artifact）"——一份把用户意图与形式规格或测试衔接起来的文档。用户意图里**可以形式化**的部分被转成形式规格；剩下**只能靠信任**的部分，被转成用于测试的非形式规格。PDD Kit 自动生成证明，表明代码满足派生出的形式规格，并为非形式规格生成高质量测试。整个过程都不需要形式方法背景。

因此，PDD Kit 的每个结果都会说明它依赖的是哪一类验证：

- **形式验证**是一个数学证明：代码在**所有可能的输入**下都满足其规格，由称为验证器的工具检查。目前 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，处理库存、促销、订单和结账；店面是编译到 WebAssembly 的 Leptos 应用。合起来大约 **5,000 行 Rust**。

本文只聚焦登录逻辑的形式验证，但同样的流程可以验证整个应用的功能正确性。PDD Kit 建议从应用里最敏感的部分开始，逐步验证。登录 bug 可能把客户账号或管理员权限交给攻击者，所以证明的投入先花在这里最值。开发者在 Chopin 里提的完整请求只有两句话：

> 验证 backend/src/handlers/auth.rs 里的登录逻辑。这是我的要求：只有密码正确才能拿到 token。只有管理员账号才能拿到管理员 token。

他们故意让请求保持粗糙。**把用户意图抓出来、把请求变成证明能检查的东西，正是 PDD Kit 的工作。**

## 第 1 步：写代码前先提问

PDD Kit 的规划工作流 pdd-plan 会读代码，然后在写任何东西之前，带着问题回到 Decisions 标签页。当一个问题取决于代码如何工作时，卡片会先解释那部分：目标、各块如何拼合、以及涉及的具体函数——这样你不打开源码也能回答。

![决策卡](https://www.hubwiz.com/blog/content/images/2026/11/img_fdd54f56f19a3370e881e77d89169b8e-800.jpg)

*图 2：第一张决策卡。"只有密码正确才能拿到 token"单独一句，也会被"拒绝所有人"的登录满足。反向也证明，才能排除它。*

这个问题看着像抠字眼，但很要紧。"只有密码正确才能拿到 token"排除的是坏情况——错误密码拿到 token；而一个"拒绝所有人"的登录完美地遵守了这个承诺。"正确密码总能成功"是排除它的另一半。形式上，第一句是蕴含（token ⇒ 正确密码），第二句是它的逆命题；合起来才是"当且仅当"。**放任 agent 自己决定，它会选一边而不告诉你**；在这里，开发者两边都选了。

## 第 2 步：一份人能读的意图地图

随着对话推进，PDD Kit 会在计划顶部维护一个"粗糙工作区"，让人不必翻回长长的聊天记录去找"当时定了什么"。它包括：被规格化的登录流程图、"什么会被证明 / 什么会被信任"的规格全景图，以及必要时的一张心智模型图。对登录，PDD Kit 画了一个售票台（图 3）。

![售票台心智模型](https://www.hubwiz.com/blog/content/images/2026/11/img_743023dbb271f5abdb4e6aa39b19e416-800.jpg)

*图 3：登录的心智模型。你发的字段决定窗口，窗口决定桌子、从而决定角色；而密码不匹配就什么都不打印。*

在它下面，意图地图把每项要求回连到开发者自己的话，并记录它是如何被敲定的（图 4）。每条记录都链接到形式规格里对它建模的那一节、以及覆盖它的测试；规格那一节会展示 Verus 契约片段，并加注解，让开发者看到形式规格如何建模自己的意图。

![意图地图](https://www.hubwiz.com/blog/content/images/2026/11/img_aed1ea32fbc800231c50e722f14b79c8-800.jpg)

*图 4：做出决策后的一条意图地图记录：只有对该账号正确的密码才能拿到 token，而且一定拿得到。流程图展示了密码检查所有可能的结束方式。*

图 2 里那张决策卡，正是 agent 会默默替你决定的那种歧义。图 5 展示了纸面上差别有多小：两种读法只在一个格子上不同——一个正确密码却拿不到 token。

![两种读法](https://www.hubwiz.com/blog/content/images/2026/11/img_95569e79f29a2b92000f672d049bdf39-800.jpg)

*图 5：同一句话的两种读法。它们只差一个格子，而这个格子改变了证明需要确立什么。*

## 第 3 步：证明登录函数

在动手实现之前，PDD Kit 会让团队对整个计划签字。它的初稿只证明了登录的核心决策——选桌子、按密码把关——而把外面的 handler 当作受信任并测试。这是个合理的默认值，也是 PDD Kit 建议的；但开发者想要更多。handler 正是 await 查询、签 token 的地方，而这段"胶水"恰恰是重构时容易悄悄换掉两行的地方。所以在意图评审时，开发者选择给登录 handler 也写一份 async 规格，让证明覆盖这段胶水，而不是信任它（图 6）。

![扩大证明范围](https://www.hubwiz.com/blog/content/images/2026/11/img_a98adb883972a2b3b1e421b91a87dd48-800.jpg)

*图 6：证明更多登录逻辑，就意味着信任更多小包装。卡片会在开发者选择之前说清这一点。*

这个选择几乎把所有东西都推进了证明，只给 handler 留下"拆请求"这一件事。一个新引入的 async 函数 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`：每次 await 成功的查询，都返回它自己那张表里该邮箱/用户名对应的那一行，或者没有。
- `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` 从外部拿到契约：

```rust
/// 按精确邮箱查一个客户。
/// 受信任，未被证明：SQL 查询在 sqlx 里执行，Verus 无法检查。
/// login_flow 的每一个客户承诺都依赖它。
#[verifier::external_fn_specification]
pub async fn ex_customer_find_by_email(pool: &sqlx::SqlitePool, email: &str)
    -> (r: Result<Option<Customer>, sqlx::Error>)
    ensures
        // 查询成功时，它返回文件里恰好对应这个邮箱的 customers 行；
        // 没有这样一行时返回 None。
        r matches Ok(found) ==> found == customer_on_file(email@),
{
    Customer::find_by_email(pool, email).await
}

```

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

```rust
/// 读时钟，算出 token 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 证明了什么、由人接受并由测试检查什么、以及没有任何人承诺的东西。

![证明边界](https://www.hubwiz.com/blog/content/images/2026/11/img_e8bf373f4d9717c4e802d6d5ef0a46b3-800.jpg)

*图 7：登录证明在哪里停下。Verus 对每个输入证明核心；人接受受信任的那一圈，测试检查它；计划列出无人承诺的部分。*

图 8 把"被证明"和"被信任"映射出来。每个信任决策都是一张独立的卡：它显示 Verus 将凭信接受的子句、开发者正在接受什么、以及假设错了会打破哪个承诺（图 9）。随后，每条被假定的子句都会在计划的"经验验证"一节拿到一项检查，在测试存在之前就写成 Given/When/Then 场景（图 10）。条目在跑过之前标着 planned，跑过之后记录命令结果和所针对的提交。

![证明地图](https://www.hubwiz.com/blog/content/images/2026/11/img_8067228f7601413f112f4a9b756590f0-800.jpg)

*图 8：登录里什么被证明、什么被信任。绿色函数由 Verus 对每个输入证明；琥珀色部分受信任、由开发者接受，并由计划 §4.1 中的测试检查。*

![信任卡](https://www.hubwiz.com/blog/content/images/2026/11/img_dee320a6a9bee9153b58af2a0e889238-800.jpg)

*图 9：check\_password 的信任卡。Verus 凭信接受这两条子句，所以由人接受它们，并由两个测试检查它们。*

![计划中的测试](https://www.hubwiz.com/blog/content/images/2026/11/img_b6f997d5b3a76503effe735897d74e0a-800.jpg)

*图 10：一个为受信任的 check\_password 计划好的测试，写在测试存在之前。计划把通过的测试标记为证据，而不是证明。*

计划对"无人承诺"的部分同样明确：登录的 future 会不会完成、超范围的时钟会不会 panic、尝试的时序与速率、以及别的端点如何读取角色。

## 第 5 步：读懂规格

团队评审的是意图工件——它是 PDD Kit 写成 Verus 契约的形式规格的平实语言版本。你可能会问：那现在是不是得有人去读证明，而不是读代码？没有人需要读，因为编码 agent 写证明、Verus 检查它的每一步。**只要 Verus 接受，证明就成立，不管有没有人读过它。** 人们评审的是"证明所依据的规格"，而这份规格短到几分钟就能学会读。

每个函数有一个 ensures 块：关于其结果 r 的陈述，必须对每个可能的输入成立。Verus 在你构建时检查它们；只要有一条子句可能对某个输入失败，构建就失败，Verus 指向那条子句。每条子句读起来像 if-then，图 11 拆解了开发者第一条要求对应的子句。

![子句解剖](https://www.hubwiz.com/blog/content/images/2026/11/img_d8ebf8edb0e6ac69fd0778b080a8db6d-800.jpg)

*图 11：login\_flow 上对应"只有密码正确才能拿到 token"的 ensures 子句。每一行都出现同一个账号 a，把密码检查与 token 绑在一起。*

注意每一行都出现同一个 `a`，它把密码检查与 token 绑定。举例：设想一个 bug——登录用 A 账号校验密码，却为 B 账号签 token。Bob 用自己正确的密码登录，却拿到 Alice 账号的 token。每一步单看都没问题，但这条子句抓住了它，因为密码检查和 token 必须指向同一个账号。**这类"接线" bug，测试集很少想到去找。**

规格还必须在**不运行它们**的情况下谈论 SQLite、bcrypt 和 JWT。它用"未解释函数"做到这点——只有名字、没有函数体：`customer_on_file(email)` 和 `admin_on_file(username)` 表示数据库持有的行，`bcrypt_verdict(password, hash)` 表示 bcrypt 会怎么说，`token_claims(token, secret)` 表示 token 携带什么。Verus 对它们一无所知，只知道第 4 步里那些受信任契约承诺的内容。证明说的是"不管数据库里有什么，登录对它的处理都是对的"，而一个受信任契约说"这次查询返回数据库里的内容"。

```rust
/// 登录查看时，数据库为恰好这个邮箱持有的 customers 行（如果有）。
/// 保持抽象：只有 `Customer::find_by_email` 的受信任契约说了它是什么。
pub uninterp spec fn customer_on_file(email: Seq<char>) -> Option<CustomerRow>;
...
/// bcrypt 对 `password` 与存储的 `hash` 给出的结论：
/// 当它就是生成该哈希的那个密码时 Some(true)，不是时 Some(false)，
/// bcrypt 读不出该哈希时 None。
/// 保持抽象：它的含义由 bcrypt 决定，通过 `check_password` 凭信取得。
pub uninterp spec fn bcrypt_verdict(password: Seq<char>, hash: Seq<char>)
    -> Option<bool>;

/// 按 bcrypt 的结论，这个密码是否是该哈希对应的正确密码。
pub open spec fn password_matches(password: Seq<char>, hash: Seq<char>) -> bool {
    bcrypt_verdict(password, hash) == Some(true)
}

```

在这些之上，`named_account(email, username)` 说明一次登录指向哪个账号：发了邮箱就用该邮箱对应的 customers 行，否则用该用户名对应的 admins 行，都没有就是 none。它写起来像 Rust，但这是一个**永远不运行的数学定义**，只出现在契约里。这种代码叫 ghost code——验证器检查它，编译器会把它从程序里抹掉。有了它，开发者那两句话的请求最终变成 login\_flow 上的 8 条 ensures 子句（图 12）。

```rust
/// 一次登录所指的账号：发了邮箱就用该邮箱对应的 customers 行（角色 "customer"），
/// 否则用该用户名对应的 admins 行（角色 "admin"），都没有就是 none。
pub open spec fn named_account(email: Option<Seq<char>>, username: Option<Seq<char>>)
    -> Option<NamedAccount> {
    match email {
        Some(e) => match customer_on_file(e@) {
            Some(c) => Some(NamedAccount {
                id: c.id@, password_hash: c.password_hash@, role: customer_role() }),
            None => None,
        },
        None => match username {
            Some(u) => match admin_on_file(u@) {
                Some(a) => Some(NamedAccount {
                    id: a.id@, password_hash: a.password_hash@, role: admin_role() }),
                None => None,
            },
            None => None,
        },
    }
}

```

![八条承诺](https://www.hubwiz.com/blog/content/images/2026/11/img_4147f09488d485e2df621f844d7804c5-800.jpg)

*图 12：两句话的请求加上"两边都要"的决策，最终变成 login\_flow 上的 8 条 ensures 子句。其中 4 条保留了今天的拒绝行为，所以店面与现有 API 测试继续有效。*

完整的契约如下（省略了文档注释的首尾）。每条子句上方是意图工件展示给团队的中文注释：

```rust
/// 整个登录，端到端 await：从请求字段到 token 或 HTTP 错误。
pub async fn login_flow(pool: &sqlx::SqlitePool, config: &Config,
    email: Option<&str>, username: Option<&str>, password: &str)
    -> (r: Result<LoginResponse, AppError>)
    ensures
        // 既没有邮箱也没有用户名：400，用今天的消息。
        email is None && username is None
            ==> (r matches Err(AppError::BadRequest(m))
                && m@ == missing_identity_text()),
        // 只有给登录所指账号、且密码正确时才有 token；
        // token 携带该账号的 id 和它那张表的角色。
        r matches Ok(t) ==> (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash)
            && token_claims(t@, config.jwt_secret@) matches Some(c)
            && c.sub@ == a.id && c.role@ == a.role),
        // 对所指账号密码正确就一定拿到 token，
        // 除非查询或签名失败给出 500。
        (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash))
            ==> (r is Ok || r matches Err(AppError::Internal(_))),
        // 登录指向一个不存在的账号：401，
        // 除非查询失败给出 500。
        ((email is Some || username is Some) && named_account(email, username) is None)
            ==> (r matches Err(AppError::Unauthorized)
                || r matches Err(AppError::Internal(_))),
        // 密码错误、且 bcrypt 能读出所存哈希：401，
        // 除非查询失败给出 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(_))),
        // 所存哈希 bcrypt 读不出来：500，且不发 token。
        (named_account(email, username) matches Some(a)
            && bcrypt_verdict(password@, a.password_hash) is None)
            ==> r matches Err(AppError::Internal(_)),
        // 管理员角色只给"按用户名找到 admins 行"且没有发邮箱的情况。
        (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),
        // 邮箱登录拿到的 token 永远携带 customer 角色。
        (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 模型：

```rust
/// 问 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）。证明一次覆盖全部。

![登录流程图](https://www.hubwiz.com/blog/content/images/2026/11/img_e05b506621174a7816a4f45873623ced-800.jpg)

*图 13：计划里登录所有可能的结束方式。*

`login_flow` 是 async 的：它会 await 一次数据库查询。Verus 能给 async 函数加契约，但有一条规则值得知道（图 14）：`requires` 在调用创建 future 时检查；`ensures` 描述 await 之后得到的值。**没有任何东西承诺 future 会完成**，所以一个挂住的查询不违反任何子句。

`login_flow` 的文档注释明确写了这一点：

```rust
/// ... 不承诺 future 会完成。
pub async fn login_flow(...) -> (r: Result<LoginResponse, AppError>)

```

![async 契约的检查时机](https://www.hubwiz.com/blog/content/images/2026/11/img_2f724041296df0c9f21485019323565e-800.jpg)

*图 14：同步 fn 与 async fn 的契约分别在什么时候被检查。*

`login_flow` 之所以能保持很短，是因为它由更小的、已被证明的部件拼成：`lookup_target` 选表；`login_core` await 查询并调用密码闸门 `decide_login`；`issue_token` 签 token，或把拒绝映射成今天的 HTTP 错误。每个部件有自己的契约，Verus 只用这些契约证明 `login_flow`，不再读它们的函数体。改了 `decide_login` 的函数体，只有 `decide_login` 需要重新证明。

最小的一块如下，以及密码闸门的开头与结尾：

```rust
pub fn lookup_target(email: Option<&str>, username: Option<&str>)
    -> (r: Result<LookupTarget, LoginError>)
    ensures
        // 发了邮箱就以邮箱为准：按该邮箱精确查 customers。
        email matches Some(e)
            ==> r == Ok::<_, LoginError>(LookupTarget::CustomerByEmail(e)),
        // 没有邮箱时，用户名把查询指向 admins，按该用户名精确查。
        email is None && username matches Some(u)
            ==> r == Ok::<_, LoginError>(LookupTarget::AdminByUsername(u)),
        // 两者都没有：因缺少身份信息拒绝。
        email is None && username is None
            ==> r == Err::<_, LoginError>(LoginError::MissingIdentity),

pub fn decide_login(target: &LookupTarget, found: Option<Account>, password: &str)
    -> (r: Result<LoginClaims, LoginError>)
    ensures
        // 没查到行：按 Unauthorized 拒绝，
        // 与密码错误的答案相同。
        found is None
            ==> r == Err::<_, 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,
        ...
        // 从 admins 表查出来的，角色文本是 "admin"。
        r matches Ok(c) && target is AdminByUsername ==> c.role@ == admin_role(),
        // 从 customers 表查出来的，角色文本是 "customer"。
        r matches Ok(c) && target is CustomerByEmail ==> c.role@ == customer_role(),

```

### login.rs 全貌

图 15 把整个规格文件 `verified/src/login.rs` 映射出来。从上往下读是四层：头部、以及 Verus 需要了解的类型；对外部世界的抽象视图；把该视图与真实代码连接起来的受信任契约；以及证明必须满足的五份契约。

![login.rs 结构](https://www.hubwiz.com/blog/content/images/2026/11/img_7a46c8987946d78f0fc9431e3317922a-800.jpg)

*图 15：login.rs 的各部分，按文件顺序。灰色是头部与类型，紫色是只出现在契约里的数学，琥珀色受信任，绿色被证明。*

两个不太显眼的部分（有删节）。`external_type_specification` 引入一个 Verus 没有定义的类型：连接池保持不透明，而 customers 行保持字段可见：

```rust
/// 连接池，对证明不透明：只有那些查询的契约说了它返回什么。
#[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` 能把每种拒绝钉到今天的状态码上的原因：

```rust
/// 一次登录为什么拿不到 token。
pub enum LoginError {
    /// 既没发邮箱也没发用户名：400 Bad Request。
    MissingIdentity,
    /// 没有这个账号，或密码不匹配：401 Unauthorized。
    Unauthorized,
    /// bcrypt 读不出所存哈希，带它的消息：500 Internal。
    UnreadableHash(String),
    /// 查询失败：500 Internal，带 sqlx 的消息。
    Database(sqlx::Error),
}

```

在计划回到你手上之前，两个评审 agent 会从意图工件出发给派生出的形式规格挑漏洞，确保这份"翻译"质量够高——规格符合你要的，也不承诺超出证明能力的东西。规格精炼在后台运行并接受用户的实时反馈，不断迭代直到评审者一致认为规格是可靠的。

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

对规格签字，就是开发者评审的终点。之后的一切——实现与证明——由机器检查，所以本文把时间花在规格上而不是证明上。开发者签字之后，一个 Build plan 阶段（图 16）把批准的计划交给 pdd-prove，后者把它变成一张小任务图（图 16）。对登录，这是 7 个任务：让 login.rs 在 backend crate 里、在 Verus 下能构建；证明决策、token 和整个流程；然后为受信任的包装与端到端登录写测试。

![Build plan](https://www.hubwiz.com/blog/content/images/2026/11/img_7d49a49a159ecf847e868e50858ac7ba-800.jpg)

*图 16：Build plan 把批准的规格变成开发机上的 7 个任务。第一个任务让 login.rs 在 Verus 下构建而不改变任何契约的承诺；它宁可停下来提问，也不削弱契约。*

每个任务都跑同一个循环：

- 一个编码 agent 写实现与证明，Verus 按派生出的形式规格检查它们。
- 受信任边界里的任何东西，都拿到计划要求的测试。
- 一个 LLM 验证器并排读计划、规格与结果，找缺口：既没有证明、也没有通过检查的要求。缺口回到编码 agent，直到一个不剩。如果规格本身有缺口——比如两条要求互相矛盾——它作为决策回到开发者。

**证明的好坏只取决于它的规格**，所以 pdd-prove 也检查规格。当一个模型自己写规格、或为了产出证明而被调过时，它容易落到弱不变量上：那些能通过验证、却几乎不排除任何情况的子句。它们证明了一些东西，只是很少是你关心的那个。我们把这叫"感觉型验证（vibe verification）"。这就是为什么让意图与 agent 对齐如此重要，也是 PDD Kit 擅长的地方。

这个循环在"不移动球门"上很严格：如果某个 async 构造在固定版本的 Verus 里表达不出来，任务会停下来问团队，而不是换成非 async 的写法或削弱契约。

**PDD Kit 怎么消除整类 bug？** 变异检查就是它防"感觉型验证"的手段：pdd-prove 在代码的临时副本里，为每条 ensures 子句种一个 bug——比如拒绝所有人、或者先查用户名再查邮箱——然后 Verus 必须在**它针对的那条子句**上拒绝每个变异体。如果某个变异体通过了，说明那条子句什么也没约束，它会作为缺口回来。

## 第 7 步：把意图与已验证的代码一起评审

任务通过后，pdd-prove 会开拉取请求。它们新增一个 `verified/` crate，包含 login\_flow、它的各个部件、它们的证明，以及带测试的受信任包装；并把真实的登录 handler 路由到 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 签名、数据库错误消息、handler 的请求拆解，都在证明之外，各自位于开发者接受的假定契约之后。针对真实 bcrypt、真实 SQLite schema 与真实路由的测试覆盖它们。
- **被假定。** Verus、Rust 编译器和 Z3 工具链，以及 Verus 的标准库 vstd。

## 为什么是 Rust

PDD Kit 目前只验证 Rust，因为 Verus 就工作在 Rust 上。如果你的代码库本来就是 Rust，没有任何迁移成本。其它语言的代码可以移植到 Rust 并用同一份规格检查；非 Rust 项目也可以通过绑定调用已验证的 Rust。

还有一个不太明显的好处：一旦不再依赖逐行评审，可读性就不再是选语言的主要理由。你可以为速度和安全性选语言，并尽可能激进地优化——**因为任何破坏规格的改动都会让证明失败。**

## 对 PDD Kit 该有什么期待

PDD Kit 是一个研究原型，目前只验证 Rust。其它语言的代码可以移植到 Rust，用同一份规格检查；非 Rust 项目可以通过绑定调用已验证的 Rust。证明仍然需要真实的投入，主要是产出证明本身；而清晰的规格是压低这份投入的关键——这就是为什么 PDD Kit 有那么多工作花在"先把意图搞对"上。他们会从"一个 bug 代价最大"的地方开始，比如登录、支付、权限，然后一块一块验证代码库的其余部分。

Pet Store 的登录只是"一个应用里的一块"：一份谁都能读的规格、一个表明代码符合它的 Verus 证明、以及为证明所信任的一切准备的测试。他们也直说了最薄弱的环节：保证的强度只等于那六个受信任片段，其中两个承担了大部分重量——`check_password` 承担所有密码承诺，两次查询承担所有"token 指向哪个账号"的承诺。测试支撑它们，但没有任何东西证明它们。他们预计这块受信任边界会随时间显著收缩，于是越来越大的代码份额能被形式验证，而他们想知道这能扩展到多远。

真正被改变的是**人们评审什么**。不再主要依赖对 agent 生成代码的逐行评审，团队评审它的含义——用平实语言——再由证明让代码守住它。计划本来就该是契约，现在 agent 真的必须遵守它了。

## 致谢

这项工作由微软研究院 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 规格加一份你批准的平实语言计划，遇到歧义就标出来而不是猜。两个评审 agent 检查规格；pdd-prove 为每条子句种一个 bug，专门抓那些"能通过验证却什么也不排除"的子句。错的规格仍然可能发生——所以 PDD Kit 强调把需求显式化、识别歧义，并让开发者在验证开始之前参与评审与批准规格。

## 我们的整理：这件事真正的门槛不在证明，在"谁签字"

原文有一句容易被略过的话：**证明是通过了，但它不自动批准新的信任项或更大的范围。** 图 6 讲的就是这个——把 handler 的胶水也纳入证明，意味着要信任更多小包装，于是卡片先把这件事说清楚，等人做选择。

把整条流程的"人的动作"抽出来，只有四个，而且都在前两步：

| 你要签的字         | 出现在哪一步     | 不签会怎样              |
| ------------- | ---------- | ------------------ |
| 两种读法都成立（当且仅当） | 第 1 步的决策卡  | agent 会自己选一边，且不告诉你 |
| 指出"这段胶水也要证明"  | 第 3 步的范围评审 | 重构换掉两行，证明照样过       |
| 逐个接受 6 个受信任片段 | 第 4 步的信任卡  | 所有密码承诺其实悬在这 6 块上   |
| 批准整份规格        | 第 6 步之前    | 证明成立，但可能证明的不是你要的   |

这也解释了为什么它能省下评审：**它把"读 3 万行 diff"换成了"读 8 条子句 + 签 6 个名"。** 后者明显更便宜，但它要求一件大多数团队现在没有的东西——有人真的去读并批准规格。

三个边界必须写在明处：

1. **只到 Rust。** 目前只有 Rust 能被验证；其它语言要么移植，要么通过绑定调用已验证的 Rust。
2. **证明不覆盖时间。** future 会不会完成、查询有多慢、超范围的时钟会不会 panic——规格里明确不承诺。并发与时序问题仍然是测试和运维的事。
3. **受信任边界是最大的风险点。** 六个片段里 `check_password` 一个就承担了所有密码承诺。测试支撑它，但没有东西证明它。

如果你现在就想用这个思路、又不想上 Verus，最小可行的版本是：把每条需求写成"如果…则…"的句子、把"只能"和"总能"两种读法分开写、把每个你决定信任的第三方函数写成一张卡（它承诺什么、假设错了会破哪条需求）、并为每张卡先写测试再写实现。**这四件事不需要任何新工具，就能拿到这套流程八成的好处。**

原文：[Formally verifying agent-written full-stack web apps with PDD Kit](https://www.microsoft.com/en-us/research/blog/formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit/?ref=hubwiz.com)（Microsoft Research Blog，Alex Lavaee & Matthai Philipose，2026-11-05）

本文由汇智网 · Software 2.0 完整编译，转载请注明出处。

> **这是「AI 编程 / Vibe Coding」专题的一部分。** 完整地图见：[AI 编程 / Vibe Coding 完全指南](https://www.hubwiz.com/blog/vibe-coding-stack/)

**相关阅读**：[AI 写测试与自己偷偷一致：变异测试与评委校准](https://www.hubwiz.com/blog/ai-tests-agree-with-bug-mutation-judge-calibration/) · [Agent 说完成了，数据库说不是](https://www.hubwiz.com/blog/agent-said-done-database-disagreed/)