PDD Kit用形式化规格验收AI全栈代码

AI 把功能写完、再补上一套全绿的测试，仍然可能交付了错误的东西：实现偏离需求，测试却跟着实现走。Microsoft Research 展示的 PDD Kit，想把自然语言计划变成机器能检查的约束，让代码必须满足约定。

他们用一个约 5,000 行 Rust 的全栈商城验证了登录逻辑。看点不是「数学证明取代测试」，而是把需求、证明和仍需信任的部分拆开，让开发者知道自己究竟批准了什么。

测试全绿，为什么还可能没实现需求

原文指出了 AI 编程的一种偏差：Agent 对需求作出自己的解释，随后编写验证这套解释的测试。覆盖率可以很好看，真正的要求却没有得到保证。

PDD Kit 采用证明驱动开发（Proof-Driven Development，PDD）：先与人确认意图，再把能够形式化的要求写成规格，由 Verus 验证代码是否对所有可能输入满足这些规格；无法进入证明的部分，交给测试提供证据。

证明保证的是代码符合规格，规格是否符合人的意图，仍然需要人判断。

它运行在 GitHub Next 的多人实时规划环境 Chopin 中。pdd-plan 负责澄清需求、记录决策和信任边界，后续通过 pdd-prove 组织 Verus 证明、测试及 LLM 缺口审查，最终把代码和验证记录放进 pull request。

这里最有价值的产物，是连接用户要求与形式化规格的「意图文档」。团队先审核它，再让工具约束实现。相较于不断增加测试数量，这个流程先追问：测试和证明到底应该保护什么？

「密码正确才能登录」，其实还少说了一半

演示项目 Pet Store 全部使用 Rust：后端采用 Axum、SQLite，处理库存、促销、订单与结账；前端使用 Leptos，编译到 WebAssembly。作者只展示其中登录逻辑的形式化验证，并未展示整个应用都已验证。

开发者针对 backend/src/handlers/auth.rs 提出两个要求：只有密码正确才能拿到 token，只有管理员账户才能拿到管理员 token。

PDD Kit 没有立刻写代码，而是先问：「密码正确，是否一定应该拿到 token？」

这不是抠字眼。「拿到 token ⇒ 密码正确」只排除了错误放行，却允许系统拒绝所有人。补上反方向的承诺，才同时约束错误拒绝。这里仍需在规格中交代账户存在、哈希可读以及依赖调用的异常路径，不能把一句双向承诺当成消除了所有失败条件。

确认后的意图文档记录了更具体的行为：账户不存在或密码错误返回 401 Unauthorized，存储的密码哈希无法读取则返回 500 unreadable hash。每项要求还会对应到形式化规格和测试。

最初方案只证明登录决策，把外围 handler 留作受信任、靠测试检查的代码。开发者希望进一步覆盖异步查询与 token 签发的衔接，于是新增带有异步规格的 login_flow，从请求字段一路约束到 token 或 HTTP 错误。

这能捕捉一种容易漏掉的接线错误：验证了 Bob 的密码，却给 Alice 签发 token。规格要求密码校验、token 的主体和角色指向同一个账户。单独检查「密码验证成功」「签名成功」，不足以保证这种关联。

证明走不到的地方，必须摊开讲

Verus 当前验证的是 Rust 代码。对于它看不到的第三方实现，以及数据库状态、系统时间等外部事实，证明需要依赖假设。这些受信任部分构成可信计算基（Trusted Computing Base，TCB）。

登录示例中，开发者批准了六类信任项：

• Customer::find_by_email 与 Admin::find_by_username，成功查询时返回各自表中对应的账户或空值。
• check_password 封装 bcrypt::verify，约定何时出错，以及 Ok(true) 的含义。
• generate_token 使用配置的 secret 签署传入 claims，签名失败返回 500。
• expiry_from_now 读取时钟，把到期时间设为恰好 24 小时后。
• database_error 将查询失败转换为当前带有 sqlx 消息的 500 响应。
• handler 外壳原样解包请求，并把字段交给 login_flow。

这些约定通过 #[verifier::external_body] 或 external_fn_specification 接入证明。后者可以为现有函数补上外部规格。

时钟示例展示了前一种方式；原文函数体用 ... 省略，下面不是完整可运行代码：

/// 读取时钟，计算 24 小时后的 token 到期时间。
/// 受信任而非已证明：chrono 的时钟不在证明范围内。
/// 时间超出范围时会 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,
{ ... }

要看的是 #[verifier::external_body]：Verus 使用 ensures 中的承诺，不检查函数体。即使这条公式参与了后续证明，时钟封装本身也没有因此得到证明。

PDD Kit 为每条假设规划 Given/When/Then 测试，运行后记录结果和对应 commit。通过测试只算经验性证据，不算覆盖所有输入的证明。

未承诺的范围也很明确：登录异步任务一定完成、查询耗时、尝试频率、异常时钟不会 panic，以及其他接口如何使用角色，都不在这份规格的保证内。

更大证明范围也有代价。覆盖 handler 的编排，需要引入更多数据库、时钟、JWT 包装契约。不能只数「证明了多少函数」，还要看证明依赖了多少假设。

我的判断

我认同它把审查重点往前移：先检查要求是否完整，再检查实现是否满足要求。对 AI 编程而言，需求中的遗漏比语法错误更容易悄悄通过验收。

但这个案例不能推出「登录已经绝对安全」。密码与 token 的账户关联可以被证明，限流、时序问题、其他接口的授权检查却未包含在承诺中。形式化验证的强度，必须连同规格和信任边界一起读。

原文称 Verus 发现了已有 bug，但给出的材料没有列出具体缺陷、验证耗时、证明维护成本，也没有与人工审查或普通测试的对照数据。「无需形式化方法背景」「比逐行审查更能扩展」目前应视为作者的工具主张与案例经验。

材料还在介绍 customer_on_file(email)、admin_on_file(username)、bcrypt_verdict(password, hash) 等无解释函数时截断，后续如何建模没有完整展开。它们是让规格谈论数据库和 bcrypt 行为的抽象名称，不代表外部实现已经被验证。

对国内常见的 React、Node.js 团队，这也不是现成接入方案。案例的证明链依赖 Rust 与 Verus，原文没有提供 TypeScript 路径。当前更容易迁移的是需求澄清和证据管理方式。

与单元测试、端到端测试相比，证明能对明确性质给出更强保证；与属性测试相比，它不依赖抽样输入，但规格编写、外部建模和维护成本也需要实际评估。这里没有足够数据替团队算出收益。

能拿来做什么

• 给 AI 下登录需求时，把成功与失败两边都写清楚：什么条件允许发 token，什么条件必须拒绝，以及依赖失败时如何响应，避免 Agent 默默补完关键语义。
• 审查前端到 Node 后端的认证链路时，明确请求身份、密码校验对象、token 主体和角色必须属于同一账户，并把这条关联纳入测试。
• 在 AI 编程计划里单列第三方依赖假设，例如密码库返回值、数据库查询语义和 JWT 签发行为，再为每条假设安排可执行检查。
• 如果项目使用 Rust，可以先挑登录决策这类敏感且边界较小的逻辑评估 PDD，并记录已证明性质、受信任契约和未覆盖要求，之后再决定是否扩大范围。