GitHub Next 介绍 PDD Kit：用数学证明验证 AI 生成代码符合规格

GitHub Next于2026年11月4日介绍了与Microsoft Research共同开发的Proof-Driven Development Kit（PDD Kit）的机制，以及将其应用于登录处理的示例。PDD Kit通过与开发者对话，将需求整理成可由机器验证的规格，并通过数学证明来确认AI智能体生成的代码满足该规格。目前它是面向Rust代码的研究用原型，仅以有限的研究预览形式提供[1]。

PDD Kit - GitHub Next

我们如何保护世界上50%的软件。

传统上，形式化方法主要用于操作系统、虚拟机监控程序和数据库等安全关键系统。我们正在使用Proof-Driven Development Kit（PDD Kit）将这一方法扩展到全栈Web应用——最常见的应用类型之一*——以形式化和实证方式验证代码的正确性与安全性。

如今，编码智能体编写代码的速度已经超过了任何人能够有效审查的速度。PDD Kit将开发者的意图转化为Verus规格，然后证明AI生成的代码对每个输入都满足该规格。

研究人员@alexlavaee、@MatthaiP39719、@Mappletons和@k_cieslak在博客中详细介绍了Proof-Driven Development x Chopin：https://t.co/EwhqTx2OjT

*44.4%的受访者从事全栈（27.3%）、后端（13.5%）或前端（3.6%）开发工作。Stack Overflow开发者调查2026，n = 25,767。——GitHub Next（@GitHubNext）2026年11月4日

GitHub Next指出，随着AI智能体代码生成量的增加，人工审查每一行代码变得越来越困难。此外，他们还指出，如果智能体误解了需求，这种误解会同时进入代码和测试中，即使测试通过，也可能无法实现预期行为。在PDD Kit中，由人决定希望软件具有的行为，并审查该内容是否已反映在规格中。

GitHub Next展示的开发流程比较。上段是人工审查智能体实现代码的流程。下段展示了使用PDD Kit的开发流程。人在计划阶段确认需求和证明的前提，智能体创建实现和证明。面向Rust的验证工具Verus检查该证明。各块的宽度仅为示意，并非工作时间的实测值（摘自GitHub Next的文章）。

通过与开发者对话，将模糊的需求转化为规格

PDD Kit在GitHub Next开发的Web应用Chopin中运行。Chopin可安装在自己的PC或服务器上，通过浏览器操作[2]。除了可以直接编辑团队共享的开发计划文档外，还可以通过聊天请AI智能体进行调查或修改文档。

PDD Kit在制定计划的过程中阅读现有代码，一边说明处理内容一边向开发者提问。根据回答，将开发者所期望的行为整理成文档。其中，能够表示为可机器验证条件的部分，会被转写为Rust验证工具Verus可处理的规格[3]。

PDD Kit的官方页面以Rust编写的Web应用“Pet Store”的登录处理为例，说明了这一规格制定流程。该应用在登录成功时，会签发记录账户标识信息以及客户、管理员等角色的令牌。开发者就这一处理向PDD Kit提出了“仅在密码正确时签发令牌”和“仅向管理员账户签发管理员用令牌”这两项要求。

在“仅在密码正确时签发令牌”这一条件下，不得在密码错误时签发令牌。然而，即使实现为拒绝所有登录、完全不签发令牌，也能满足这一条件。因此，PDD Kit在进入实现之前确认道：“是否也要求密码正确时必定签发令牌？”

开发者表示，也要求密码正确时签发令牌。不过，即使密码正确，数据库查询或对令牌的签名也可能失败。因此，在最终的规格中，规定这些处理失败时，可以返回服务器错误来代替令牌。

就这样，登录处理的规格中纳入了8个条件[4]。例如，其中一个条件是：用于核对密码的账户与令牌所表示的账户必须一致。通过这一条件，可以捕捉到用自己的密码通过认证、却签发了他人令牌这类缺陷。

官方页面交互式解说画面（部分）。在左侧，可以切换登录请求是否包含电子邮件地址或用户名、账户是否已注册、密码是否正确、数据库查询或签名处理是否失败。可以确认登录结果以及8个规格条件中哪一个适用，右侧则会高亮显示相应条件。在“Plant a bug”标签页中，还可以确认缺陷示例与捕捉该缺陷的条件之间的关系。

在实际制定规格时，PDD Kit会用图示说明处理流程，帮助开发者确认规格。为Verus编写的规格也会附上说明各条件的英文注释。开发者确认要求是否按意图表达，并批准规格。

智能体生成证明，Verus进行检查

编码智能体根据已批准的规格生成实现，并创建证明，以表明该实现满足规格。Verus检查该证明，确认在既定前提下，对于规格所涵盖的所有输入，条件均成立。这种形式验证不同于针对个别输入执行代码并观察结果的测试。

不过，如果规格条件过于宽松，即使代码违背意图，证明也能通过。因此，PDD Kit会在代码的工作副本中，针对规格的每个条件逐一故意植入违反该条件的缺陷。并确认Verus能够将该缺陷检测为对目标条件的违反。

证明范围之外的处理通过测试确认

本次登录处理中，数据库查询、bcrypt密码核对、时间获取、对令牌的签名等使用了其他库。不过，这些库内部的处理本身不在本次证明范围内。因此，在假定各处理按规格预期工作的前提下，证明登录处理的正确性。

关于这些证明前提，PDD Kit会在实现前的计划阶段向开发者说明各处理被假定满足的条件。还会说明当该条件不成立时会失去哪些保证，并逐项请求批准。同时，也会规划用于确认各假定条件的测试。

即使是证明范围内的处理，所保证的也仅限于规格中写明的范围。在本次规格中，保证的是登录处理返回响应时，其结果满足条件。并不保证处理必定完成，也不保证响应需要多长时间。

确认验证结果并合并，变更后也继续验证

用于审查的LLM会对照计划、规格和验证结果，检查是否已通过证明或测试确认实现满足各项要求。如果有要求未能通过证明或测试任一方式确认，则要求编码智能体进行处理。如果规格本身存在矛盾，仅修改实现无法解决，因此PDD Kit会请开发者作出判断。

通过证明检查和测试后，PDD Kit会创建包含实现、证明和测试的拉取请求。其中还会记载已证明的内容、关于证明范围之外处理的前提、测试结果以及保证范围。开发者会对照所期望的行为确认内容并合并。合并后，还会将Verus验证和测试纳入持续集成（CI），在每次代码变更时确认仍满足同一规格。

本次案例仅限于一个应用的登录处理。GitHub Next表示，创建证明目前仍然费时费力，同时正在探索能否应用于更广泛的范围。