微软PDD Kit用形式化验证破解AI代码审查

当AI编程智能体一次就能交付数万乃至数十万行代码，谁来确认它真正实现了开发者的要求？微软研究院介绍的PDD Kit给出了一条形式化验证路径：先把人的意图变成可检查的规格，再证明代码满足这些规格；证明无法覆盖的部分，则交给测试。在一个名为Pet Store的全栈Web应用中，团队用这套工具验证了登录逻辑，开发者负责审阅意图，没有逐行阅读生成的代码。其意义在于，将审查重点从庞大的实现细节转向需求、证明范围与信任边界。

代码越来越多，测试通过仍可能偏离需求

当前不少团队会先与智能体讨论计划和测试方案，确认后再让它实现功能。这份自然语言计划本应成为双方的契约，但实际执行中缺少强制约束：智能体可能实现一个略有不同的功能，再编写恰好适配自身实现的测试。结果是持续集成流程中的测试数量不断增长，覆盖率看起来不错，需求与交付之间的偏差却要等到缺陷报告或棘手的边界情况出现时才暴露。原文将问题归为两类：遗漏明显必要的行为，以及执行明显错误的行为。

测试只能运行程序可能行为中的一小部分。形式化证明则针对明确写下的规格，检查代码是否对每一种可能输入都满足要求。过去，这类工作往往需要专家、陌生的语言，以及体量数倍于代码、可能耗时多年完成的证明。微软研究院认为，编程智能体如今既能协助生成证明，也能帮助编写形式化规格，让这种方法有机会进入日常软件开发。团队将其称为证明驱动开发，即Proof-Driven Development（PDD），PDD Kit就是配套工具；它与PDD的关系，类似Spec Kit与规格驱动开发的关系。

从共同确认意图，到区分证明与证据

PDD Kit运行在GitHub Next的Chopin中，这是一个支持团队与智能体在同一份共享文档内实时协作的规划环境。工作流分为两部分：首先，成员用自然语言审阅意图，工具像细心的审查者一样提问、解释相关代码，并把答案记录在连接用户需求与规格或测试的意图文档中；随后，可形式化的需求被转成形式化规格，其余需要依赖信任的部分被整理为用于测试的非形式化规格。工具据此自动生成证明与测试，目标是让没有形式化方法背景的工程师也能参与。

目前承担证明检查的是Verus，一种面向Rust的证明语言。其共同开发机构包括微软研究院、卡内基梅隆大学、VMware Research、苏黎世联邦理工学院、马克斯·普朗克软件系统研究所（MPI-SWS）、悉尼新南威尔士大学、得克萨斯大学奥斯汀分校、密歇根大学、不列颠哥伦比亚大学、威斯康星大学麦迪逊分校，以及魏茨曼科学研究所。对于第三方密码学库、用户界面等证明难以触及的部分，PDD Kit采用经验验证，包括单元测试、端到端测试、终端自动化、浏览器智能体，以及处理浏览器无法驱动操作的计算机使用智能体。测试通过只说明尝试过的输入得到预期结果，因此工具将其标为“证据”，而非“证明”。

两种验证方式的分界涉及可信计算基（TCB），即证明过程中假定其行为符合描述的代码。PDD Kit会明确展示这条边界，并要求开发者逐项认可。这里的审查责任并没有消失，而是变得更具体：哪些性质得到了数学保证，哪些依赖外部组件正确工作，哪些只有运行测试支持，都需要被清楚区分。即便证明成立，如果规格没有准确表达需求，仍不能据此认定产品满足了用户意图。

约5000行全栈应用，先验证登录要害

为了展示与已有代码库的集成，团队构建了完全用Rust编写的Pet Store。后端采用Axum与SQLite，处理库存、促销、订单和结账；店面前端使用Leptos，并编译为WebAssembly，前后端合计约5000行Rust代码。此次介绍聚焦登录逻辑，并非宣称整个应用已经完成形式化验证。团队表示，同样的流程可以用于验证整个应用的功能正确性，并建议从最敏感部分开始逐步推进：登录缺陷可能让攻击者取得客户账户或管理员权限，因此优先投入证明工作有明确价值。原文称，Verus帮助加固了代码并发现既有缺陷，最终证明的是相对于所定规格不存在登录错误。

开发者在Chopin中的请求只有两句话，要求验证backend/src/handlers/auth.rs中的登录逻辑，并提出两个约束：只有密码正确才能获得令牌，只有管理员账户才能获得管理员令牌。PDD Kit的规划工作流pdd-plan先读代码，在写入任何内容之前，通过Decisions标签页提出问题；如果问题依赖代码行为，决策卡会先解释目标、组件关系和涉及的具体函数。最关键的澄清是，“只有密码正确才能获得令牌”也能被一个拒绝所有人的登录系统满足。要排除这种情况，还要确认“正确密码总能成功”。前者是“获得令牌意味着密码正确”，后者是其逆命题；两者合起来才构成充要关系，开发者最终选择同时证明两个方向。

为了让这些决定可追踪，计划顶部持续更新工作草稿，包括登录流程图、哪些内容会被证明或被信任的说明，以及辅助理解的模型。工具把登录比作售票窗口：请求字段决定窗口，窗口决定查询哪张表并对应何种角色，密码匹配后才能出票。下方的意图映射将每条要求关联到开发者原话、最终决定、形式化规格和测试，并为Verus契约片段添加说明。原文展示的两种需求理解，在对照表里只相差一个单元格——密码正确却没有令牌——但这一处差异就改变了证明必须建立的性质。

扩大证明范围，也要重新确认信任边界

正式构建前，PDD Kit要求团队批准整体计划。最初的方案只证明登录中心的决策，包括选择数据表和依据密码控制访问，外围处理器仍作为可信代码接受测试。这也是工具推荐的默认方案，但开发者希望进一步覆盖处理器，因为数据库查询的异步等待与令牌签名发生在这里，重构时交换两行代码就可能引入问题。开发者因此为登录处理器选择了独立的异步规格。修订后，一个名为login_flow的新异步函数承载从请求字段到令牌或HTTP错误的契约，原处理器主要负责拆解请求。工具再次提交计划供确认，因为扩大证明范围也意味着需要信任更多小型封装，之前认可的意图不能自动等同于批准新增信任或扩大的范围。

证明仍有清晰的止步点。bcrypt的哈希计算、sqlx的查询和jsonwebtoken的签名位于外部crate中，验证器无法直接检查；SQLite当前保存的内容和时钟读数属于外部输入，不能由程序自身代码确立；现有规格描述的是登录返回时应得到什么，并不保证查询一定结束，也不保证足够快。因此，查询挂起或缓慢并不违反该规格。错误提示是否有帮助、界面是否易于理解等判断仍需人参与，而没有写进规格的要求也不会自动获得证明。这些限制决定了，“对所有输入成立”必须始终与具体规格及其假设一起理解。

PDD Kit展示的后续方向，是先对高风险模块建立可审阅的意图与证明，再逐步扩展到更多应用功能。对AI代码审查而言，它提供了一种更可扩展的分工：人负责确认需求及可接受的信任范围，智能体协助生成实现与证明，验证器检查形式化性质，测试补充外部依赖和交互体验的运行证据。其实际价值取决于这套链条能否持续保持一致，尤其是在需求变更和代码重构之后，让已经确认的契约仍然约束最终交付。