AI 编程

AI 写的代码不用逐行读：微软 PDD Kit 用证明替代评审

计划本该是 agent 必须遵守的契约，却没什么强制它遵守。PDD Kit 先把意图谈成可读规格，再让机器证明代码对每个输入都满足它，证不到的地方退回测试。

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

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

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

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

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

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

速览

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

图 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 标签页。当一个问题取决于代码如何工作时，卡片会先解释那部分：目标、各块如何拼合、以及涉及的具体函数——这样你不打开源码也能回答。

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

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

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

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

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

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

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

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

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

第 3 步：证明登录函数

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

图 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 从外部拿到契约：

/// 按精确邮箱查一个客户。
/// 受信任，未被证明：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 子句，从不读函数体：

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

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

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

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

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

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

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

第 5 步：读懂规格

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

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

图 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 步里那些受信任契约承诺的内容。证明说的是"不管数据库里有什么，登录对它的处理都是对的"，而一个受信任契约说"这次查询返回数据库里的内容"。

/// 登录查看时，数据库为恰好这个邮箱持有的 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）。

/// 一次登录所指的账号：发了邮箱就用该邮箱对应的 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,
        },
    }
}

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

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

/// 整个登录，端到端 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 模型：

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

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

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

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

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

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

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 需要了解的类型；对外部世界的抽象视图；把该视图与真实代码连接起来的受信任契约；以及证明必须满足的五份契约。

图 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 能把每种拒绝钉到今天的状态码上的原因：

/// 一次登录为什么拿不到 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 和整个流程；然后为受信任的包装与端到端登录写测试。

图 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 个名"。 后者明显更便宜，但它要求一件大多数团队现在没有的东西——有人真的去读并批准规格。

三个边界必须写在明处：

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

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

原文：Formally verifying agent-written full-stack web apps with PDD Kit（Microsoft Research Blog，Alex Lavaee & Matthai Philipose，2026-11-05）

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

这是「AI 编程 / Vibe Coding」专题的一部分。 完整地图见：AI 编程 / Vibe Coding 完全指南