GitHub Next 推出 PDD Kit:用形式化验证为 AI 生成的全栈代码兜底

0xkarasy · x · 2026-11-05

GitHub Next 与 Microsoft Research 合作发布研究原型 PDD Kit(Proof-Driven Development Kit),目标是解决一个越来越尖锐的问题:编程 agent 写代码的速度已远超人类逐行审查的能力,合并代码时你到底在为什么背书?

思路转变:形式化方法传统上只用于操作系统、hypervisor、数据库等安全关键系统,现在被推广到全栈 Web 应用——据 Stack Overflow 调查,约 44.4% 的开发者从事全栈/后端/前端工作,覆盖面极广。
工作方式:PDD Kit 把开发者的意图转化为 Verus 规约(specification),然后数学证明 AI 生成的代码对所有输入都满足该规约,证明覆盖不到的地方辅以测试。
人机分工:人负责「软件应该做什么」的判断与决策(规划、评审),逐行正确性检查交给形式化证明。

这相当于把 agentic 开发中的评审瓶颈,从人工 line-by-line review 换成了机器可验证的数学保证。团队成员包括 Alex Lavaee、Matthai Philipose、Maggie Appleton、Krzysztof Cieślak,详细博客已发布。

「编程与Agent」频道最新