微软发布PDD Kit：用形式化验证约束智能体生成代码

摘要：微软研究院发布研究原型 PDD Kit，将证明驱动开发（Proof-Driven Development）引入智能体编程流程：开发者先审阅自然语言意图，系统再生成 Verus 规范、形式化证明和边界测试，由 Z3 确定性验证代码是否在所有输入下满足批准后的规格。Pet Store 登录案例显示，该方案可捕获既有缺陷，并把审查重心从逐行代码转向意图与信任边界；但其保证仍受 Rust、Verus/Z3 工具链以及数据库、bcrypt、时钟和 JWT 签名等受信组件约束。

---

微软研究院发布研究原型 PDD Kit，尝试解决智能体编程中最棘手的可扩展性问题：生成代码已达数万甚至数十万行，团队无法再依赖逐行审阅，而由智能体自己编写的测试又可能只是验证其实现，而非开发者真正提出的需求。

PDD Kit 的核心不是再生成一套测试，而是把开发计划升级为可机器检查的契约：先由开发者确认意图，再生成 Verus 形式化规范与证明；证明无法覆盖的部分，例如第三方库、数据库状态、UI 和系统时钟，则保留为明确标注并经人工接受的信任边界。

从自然语言意图到形式化契约

整个流程分为规划、证明与持续交付三个阶段。

pdd-plan 会先读取现有代码，在生成实现前提出决策问题，并生成一份人类可读的 intent artifact。它连接用户原始需求、形式化规范和测试计划，并明确区分：

• 可形式化的需求被转换为 Verus 规格；
• 难以形式化的需求被转换为非形式规格和测试；
• 每项信任假设都需要开发者单独批准；
• 规格与需求冲突或存在歧义时，流程停止并请求决策。

这解决了一个容易被形式化工具忽略的问题：证明只能说明代码符合规格，不能证明规格符合人的真实意图。登录要求“只有正确密码才能获得令牌”看似明确，实际只表达了 token ⇒ correct password；一个拒绝所有用户的登录同样满足它。PDD Kit 通过“双向确认”补上逆向蕴含 correct password ⇒ token，使完整要求成为充要条件。

Verus 如何把登录逻辑纳入证明

案例项目是一个约 5,000 行 Rust 的全栈 Pet Store：后端使用 Axum 与 SQLite，前端使用 Leptos，并编译为 WebAssembly。演示重点是认证逻辑，而不是将形式化方法强行覆盖整个应用。

PDD Kit 将登录流程拆为五个主要函数：

• lookup_target：根据邮箱或用户名选择客户或管理员数据表；
• decide_login：判断账户是否存在以及密码是否匹配；
• issue_token：签发令牌或映射为 HTTP 错误；
• login_core：组合查询、密码判断与令牌签发；
• login_flow：覆盖从请求字段到令牌或错误的完整异步流程。

每个函数都带有 requires 与 ensures 契约。后置条件要求密码校验对象、令牌 sub 和角色必须指向同一个账户。例如，如果程序用 Bob 的密码完成校验，却为 Alice 签发令牌，同一个账户变量 a 会同时出现在密码、主体和角色约束中，使 Verus 能够拒绝这种跨账户接线错误。

数据库内容、bcrypt 判定和令牌内容则通过 uninterpreted function 建模。这些函数只有名字而没有可执行实现：验证器不需要知道 SQLite 或 bcrypt 的内部算法，只依据外部契约推理。相关定义属于 ghost code，只在规格与证明中参与检查，编译后不会进入生产二进制。

对于 async fn，requires 在调用创建 Future 时检查，ensures 在 Future 返回结果时成立，但规格不保证 Future 最终完成。因此，SQL 查询永久挂起或响应过慢，不会违反功能正确性契约；活性、超时和速率限制仍需另行验证。

信任计算基是安全性的真实上限

PDD Kit 把证明能够覆盖的部分与必须依赖假设的部分明确分开。登录案例中，Verus 证明五个核心函数；但以下六类组件仍位于 Trusted Computing Base（TCB）之外或边界之上：

1. 客户和管理员数据库查询；
2. 封装 bcrypt 的 check_password；
3. JWT 令牌签名；
4. 系统时钟与过期时间计算；
5. 数据库错误消息映射；
6. HTTP 请求解包与字段转发。

外部函数通过 external_fn_specification 声明假设契约，外部函数体则可使用 external_body，让 Verus 检查契约但不读取实现。PDD Kit 为每条假设生成 Given/When/Then 测试，并要求开发者接受每项信任及其失效后果。

这套设计比“全部已验证”的宣传更精确：安全性依赖于受信契约是否真实成立。尤其是 check_password 和数据库查询承担了大部分密码与账户身份保证，测试只能提供经验证据，不能替代证明。

变异检查对抗“氛围式验证”

LLM 很容易生成能够通过验证、却没有实际约束力的弱规格，也就是 PDD Kit 所称的 vibe verification。为此，pdd-prove 会针对每条 ensures 子句注入一个定向变异，例如让所有登录都失败，或颠倒邮箱与用户名的查找顺序。

如果某个变异没有被 Verus 拒绝，对应子句就未发挥预期约束作用，流程会把它作为缺口退回。只有变异被逐条杀死，才能降低“形式上通过、实际上没证明关键行为”的风险。

在证明阶段，模型负责编写代码、规格和证明，但最终裁决由 Verus 与 Z3 确定性完成，不依赖另一个语言模型自我批准。LLM gap review 仅用于横向检查需求、规格与验证结果之间是否仍存在未覆盖项。若现有 Verus 版本无法表达某个异步结构，任务会停止并要求团队处理，而不是静默换成较弱契约。

工程收益与现实成本

PDD Kit 的直接收益是改变审查对象：人类审阅意图、形式化规格和信任边界，机器检查实现是否符合契约。证明失败后，CI 可以像处理失败测试一样阻断合并；对于已被证明覆盖的示例测试，团队还可以删除重复用例，让测试套件更聚焦于受信组件和端到端行为。

但这套流程并非“写完需求后自动获得全程序正确性”。证明成本主要来自规格设计和证明编写，而非 Verus 最终执行。小模块通常需要数秒，较大代码库可能达到数分钟；模型可以降低证明编写门槛，却不能消除 SMT 求解、异步建模和外部依赖带来的复杂度。

该原型目前仅支持 Rust，因为 Verus直接验证 Rust。若主系统使用其他语言，可以将关键逻辑移植到 Rust，再通过绑定调用，但这会增加接口、行为一致性和运维复杂度。Verus、Z3、vstd 以及所依赖的编译器工具链本身也处于信任假设之中。

此外，形式化证明不自动覆盖活性、吞吐量、可用性、安全响应时间或用户体验。登录 Future 是否最终完成、查询是否超时、暴力破解限速是否有效、角色在其他端点是否被正确读取，都不在该登录证明的承诺范围内。

开发者落地建议

1. 从高风险边界开始：优先覆盖登录、支付、权限和数据授权，而不是试图一次性证明整个代码库。
2. 先消除需求歧义：逐条确认充要条件、错误语义和角色映射，避免把错误规格精确地证明下来。
3. 显式记录 TCB：每个外部函数都应说明依赖假设、失败后果和对应测试，不可用“已验证”掩盖边界。
4. 把 Verus 接入 CI：证明必须成为持续门禁，而不是一次性研究演示，否则后续代码改动会迅速使契约失效。
5. 保留经验验证：第三方密码库、数据库语义、时钟、UI、终止性和性能仍需专项测试与独立审计。
6. 把 PR 当作验证收据：逐项标注哪些行为是形式化证明、哪些是测试证据、哪些尚未作任何承诺。

PDD Kit 的意义在于把智能体开发从“生成后靠人读”推向“生成后由确定性工具对批准后的契约负责”。它尚不能消除代码审查，却能重新分配审查注意力：人负责意图和信任边界，机器负责可判定的功能性质。

---

消息来源：Microsoft Research AI (2026-11-05)

—— 完 ——

主题标签： #PDD Kit 关注 #形式化验证 关注 #Verus 关注 #Rust 关注 #编码智能体 关注