微软研究院公布PDD Kit原型，尝试将证明驱动开发引入AI编程：先把开发者意图写成规格，再由智能体生成实现与证明，最后用Verus/Z3对Rust代码进行形式化验证。该案例聚焦登录逻辑，强调证明依赖明确的假设与可信组件，并不能替代测试或消除所有信任边界。
微软研究院于2026年11月5日披露一项名为PDD Kit的研究原型，试图为智能体编程增加一道不同于测试的约束：让开发者先确认软件应当做什么，再由智能体生成实现和数学证明，交给形式化验证工具检查代码是否符合约定。
在微软公布的案例中，研究团队将这套流程用于一个约5000行Rust代码的Pet Store全栈商店应用，重点展示登录逻辑的验证。它并不是整个应用“没有漏洞”的证明，也不是已经普遍适用于各类语言和项目的成熟产品。其保证有明确前提：规格表达正确，受信任组件按约定工作，验证工具链可靠。
这一尝试针对的是AI编程中的一个实际难题：智能体可以快速生成实现，也可以围绕自己的实现编写一套能够通过的测试，但两者一致，并不意味着它们符合开发者最初的要求。
从“密码正确才能登录”里的歧义开始
PDD是Proof-Driven Development，即证明驱动开发。微软将PDD Kit放在GitHub Next的Chopin环境中使用。根据Chopin官方项目介绍，它是供团队成员与智能体共同编辑、讨论计划的实时协作研究原型，能够记录决策及其来由；这与已经完成产品化的开发平台仍有区别。
Pet Store案例的起点只有两项粗略要求：只有密码正确才能获得令牌；只有管理员账户才能获得管理员令牌。
第一句话看似清楚，却留下了关键缺口。一个拒绝所有人的系统，也满足“密码错误的人拿不到令牌”。如果开发者还要求合法用户能够成功登录，就必须另行表达：正确密码应当带来成功结果，并明确数据库查询或令牌签名失败时如何处理。
PDD Kit的规划流程会先提出这些问题，把答案写成自然语言的意图记录，再映射为Verus规格和测试计划。人类需要批准的不是一句笼统的“保证安全”，而是账户如何选择、密码如何匹配、角色如何赋予、异常如何返回，以及哪些依赖只能接受假设。
在这个案例中，如果请求包含电子邮件，登录流程应查找客户账户；没有电子邮件、只有用户名时，才查找管理员账户。这样细小的选择也会进入规格，而不是留给生成代码的智能体自行决定。
检查证明的，不是另一个语言模型
PDD Kit采用的Verus是面向Rust的验证工具。其项目文档说明，开发者描述代码应满足的规格，工具借助求解器进行静态验证，而不是等程序运行时再增加检查；目前它支持的是Rust的一个子集，仍处于活跃开发阶段。
在PDD Kit的流程里，语言模型参与生成规格、代码和证明，但最终是否通过，由Verus机械检查决定。微软介绍，该检查使用Z3求解器，判断实现是否在形式模型与既定假设下，对所有受覆盖输入满足所写性质。这与抽取若干输入运行测试，或请另一个模型阅读代码后给出意见，并不是同一种保证。
登录验证尤其需要约束不同步骤之间的关联。例如，系统即使分别完成了“密码验证”和“令牌签发”，仍可能错误地用甲的密码验证结果，为乙签发令牌。案例中的规格要求，密码所对应的账户、令牌中的账户标识和角色必须一致，以排除这种连接环节的错误。
微软称，案例最终为登录总流程及其组成部分建立了契约和证明，覆盖账户查找目标选择、密码判断、令牌处理，以及相应的HTTP错误路径。开发者还选择为异步登录流程建立规格，把部分原本只能信任的编排逻辑也纳入证明范围。
但这不意味着“只要密码正确就永远能拿到令牌”。公开契约保留了查询或签名失败返回服务器错误的情况；异步操作是否最终完成，也不在这些后置条件的保证内。
数据库、密码库和时钟，仍在证明之外
形式化证明不能自动消除全部信任。PDD Kit会把可信计算基，也就是证明所依赖却没有在其中证明的部分，明确列出来，要求开发者接受相应契约，再以测试提供经验性支持。
在Pet Store案例中，这些依赖包括客户和管理员数据库查询、封装bcrypt的密码校验、JWT令牌签名、系统时钟及到期时间计算、数据库错误映射，以及请求字段的解包和传递。
例如，登录证明可以建立在“查询返回指定电子邮件对应的账户”这一前提上，进而证明令牌绑定正确账户。但如果实际查询并未兑现这个前提，登录逻辑内部的证明不会替数据库实现承担保证。同样，密码相关性质依赖bcrypt封装契约成立，而不是PDD Kit已经证明了密码库本身正确。
微软表示，流程会针对这些假设安排真实组件测试，并区分尚未执行的测试计划与已经运行的结果。测试通过仍只是对已尝试情形的证据，不会变成覆盖所有输入的数学证明。验证器、Rust编译器、Z3和Verus标准库，也属于整条保证链需要信任的基础。
还有一些风险根本没有被这份登录规格承诺排除：查询挂起或响应过慢、异常时间值导致的panic、登录尝试的频率与时序问题，以及其他接口如何使用角色信息。没有写进规格的要求，不会因为存在一份证明就自动获得保护。
防止“证明了一个没有用的命题”
证明可能完全正确，规格却过于宽松。对此，PDD Kit除了安排模型检查需求与规格之间的缺口，还采用变异检查：在临时代码副本中人为引入针对特定契约条款的错误，例如拒绝所有用户，或颠倒账户查找的优先顺序，再要求Verus在对应条款上拒绝这些变体。
如果错误实现仍能通过，就需要重新检查规格是否真正约束了目标行为。不过，这种检查也不能证明所有需求都已被完整表达。微软在FAQ中承认，错误规格仍然可能出现，开发者对意图和信任边界的审核不可省略。
团队还描述了后续维护机制：把Verus检查与经验性测试一起接入持续集成，让未来由人或智能体提交的修改继续满足相同契约。证明因此不只是一次演示的结果，而是可以随代码变更持续检查的约束；前提是团队没有随意削弱原有规格。
从研究示范走向日常开发，还有哪些距离
AI生成、外部检查器核验，是近期软件验证研究中的一条共同路线。此前本站报道的Anthropic与Theorem形式验证研究针对特定构建的软件二进制生成安全证明；PDD Kit此次展示的重点，则是把开发者意图转成规格，并将Rust应用的登录实现纳入同一工作流。二者的验证对象与适用条件不同，不能直接拿规模数字比较能力。
就PDD Kit本身而言，微软明确将其定位为研究原型，目前只验证Rust。团队建议从登录、支付、权限等错误代价较高的部分入手，再逐步扩大覆盖，而不是一次宣称验证完整系统。证明生成仍需投入，可信边界能缩小多少、流程能扩展到多大代码库，仍是待研究的问题。
这份公开案例展示的是一种审核重心的变化：开发者不再只问“生成的代码看起来对不对”，还要明确“系统必须满足哪些性质，哪些前提仍靠信任”。它提供了比单纯测试更强的、针对既定规格的保证，但没有取消需求判断、集成测试和安全审查，也不能被理解为AI编程已经获得普遍的无漏洞承诺。