AREX Feed Article
微软研究院发布 Proof-Driven Development Kit：把开发者意图写成形式化规范，再证明 AI 生成的代码符合它
北京时间 10 月 21 日 23 时 58 分，GitHub 的前瞻研究团队 GitHub Next 在 X 上宣布推出 Proof-Driven Development Kit（PDD Kit）。这套工具来自 Microsoft Research，思路是：先把开发者的意图翻译成形式化规范（formal specification），再用形式化验证（formal verification）证明 AI 生成的代码符合规范，并已与面向 Rust 的证明工具 Verus 以及 GitHub Next 自己的多人规划环境 集成（）。约三小时后，Microsoft Research 官方账号 @MSFTResearch 在北京时间 22 日凌晨 3 时 19 分发帖确认了同样的内容，并把问题摆在最前面：「AI 智能体写的代码越来越多，开发者如何保证代码是正确的？」（）
GitHub Next 在公告里把目标写成：「一个经过验证的软件工厂（verified software factory）——工程师审的是规范，而不是代码。」GitHub 官方账号在八分半钟后跟进发帖，称这套组合能让团队「把 AI 生成的代码送进生产环境而不必逐行审查」，并「现已进入研究预览（research preview）」（）。两则公告都把现场演示安排在了 10 月 28–29 日的 GitHub Universe 大会。
从意图到证明：PDD Kit 的工作流
GitHub Next 的公告按顺序拆解了这套流程。以一个应用的登录流程为例：PDD Kit 会与开发者讨论代码、在过程中推断意图，然后提出一份用 Verus 写成的形式化规范——GitHub Next 称 Verus 是「Rust 的证明语言」；开发者批准规范之后，Verus 验证器自动证明代码满足它，「针对每一种输入」。证明无法成立的场合，工具回退到经验性验证：测试加计算机操作智能体（computer-use agents，CUA）。
六分钟后，在 Microsoft Research 从事应用 AI 工作的 Alex Lavaee（其 X 账号资料如此标注）也发帖补充了产品侧的描述：你用日常英语描述想构建什么，PDD Kit 捕捉你的目标——团队称之为意图（intent）——再用验证器针对所有可能输入证明代码符合它。「你不会审查一行代码，也不会审查证明本身。你审查的是你的计划，以及用自然语言写下的目标。」（）
他用登录给出了证明与测试的差别：测试只能检查「正确的密码能让用户登录」，而叠加上证明之后，可以验证「不存在任何错误密码允许登录的情形」。GitHub Next 为这套流程给出一句简短定位——「No vibe verification」，与「凭感觉写码」（vibe coding）划清界限；Chopin 项目页则把「把模糊想法直接丢给编码智能体」的产物称作 vibe-coded slop（）。
审查瓶颈：最佳 AI 审查员也漏掉两成以上的 bug
推动这套工具的动机写在 Lavaee 的帖文里：审查跟不上生成。他的说法是，智能体写的代码已经超过任何人能审查的量，多数人最终只是浏览一遍 PR（pull request，拉取请求）或 diff 就合入——「现有的审查方法并不能证明代码正确，也不能证明它做了我们要它做的事」。
他引用了一份 2026 年 10 月 9 日提交至 arXiv 的论文《(When) Should a Software Factory be Lights-off? Benchmarking Code Review Agents on Bug Detection》，并将其标注为 Microsoft Research 与 CMU 的合作工作（）。论文构建了 CRBugBench 基准：从仓库历史中挖掘经人工确认的 bug，为每个 bug 配上引入它的 PR，组成 98 个开源 GitHub 仓库上的 1,000 个审查任务，外加一家大型公司专有仓库中的 800 个任务。
按这份基准，最佳审查智能体（claude-opus-5 配合 copilot-cli）能在前五条评论里捕获 71.9% 的 bug，比五个月前的 opus-4.6（47.7%）进步明显，但仍会漏掉人类发现的 20% 以上 bug，在更需要项目上下文的专有工业仓库上表现还会明显下滑。论文摘要开宗明义：开发者花在审查代码上的时间已经超过写代码，人类审查速度正在落后于智能体的生成速度。这正是 PDD Kit 想绕开的环节——把保障从「读完每一行」换成「证明每一行都符合规范」。
Verus：不用学新语言，证明就用 Rust 写
被 PDD Kit 选中的 Verus 并非新面孔。Microsoft Research 的「Practical System Verification」项目页介绍，Verus 是一个基于 SMT（satisfiability modulo theories，可满足性模理论）求解器的 Rust 程序形式化验证工具：程序员直接用 Rust 语言表达证明与规范，不需要学习一门新语言；同时 Verus 利用 Rust 的线性类型和借用检查，在证明中表达所有权与分离关系（）。项目代码开源在 verus-lang/verus 仓库（）。
GitHub Next 在公告中强调，PDD Kit「今天就能用于 Rust。不需要新语言，也不改变你产出底层代码的方式」，目的就是把形式化方法的门槛降下来。微软研究院自己也在往同一个方向铺路：上述项目页写道，团队正在探索用大语言模型降低用 Verus 编写证明的成本，配套的证明合成基准 Verus-Bench 与 VeruSAGE-Bench 已在 microsoft/verus-proof-synthesis 仓库开源。
Chopin：让整支团队围着同一份计划文档工作
Chopin 是这场发布里的另一半。按 GitHub Next 项目页的描述，它是一个实时多人、围绕 GitHub 仓库组织的智能体规划环境：团队在基于 MDX（Markdown 的扩展格式）的编辑器里共同撰写计划，仓库可见的人都能参与；文档任意位置可以开评论线程来驱动智能体修改计划；每个决策都留有持久日志，事后改写文档也不会抹掉「当时决定了什么」；它还提供 MCP（Model Context Protocol，模型上下文协议）服务器，允许任何智能体接入（）。
项目页对现有规划工具的批评解释了它为什么存在：终端里的计划「至多是一大块不可编辑的静态文本」，市面工具几乎都是单人体验，而且没有决策留痕——「对严肃的软件，我们需要严肃的审计记录」。Chopin 的开源仓库同样写明：它是实验性研究软件，不是受支持的 GitHub 产品（）。
集成本身在两边的公告中都有明说：GitHub Next 写道「PDD Kit 已与 Chopin 集成，你可以以团队方式做计划」；@MSFTResearch 的帖文同样强调，这次集成把形式化方法带进了团队的 AI 辅助开发工作流。
有限预览、Rust 边界，和一个尚无回复的问题
需要先说明这次发布的成色：以上能力描述全部来自 GitHub、Microsoft Research 两方账号及团队成员的公告，属于当事方口径；本文引用的材料中，没有独立第三方的验证结果。GitHub 官方账号称「现已进入研究预览」，Lavaee 的措辞更保守——「有限研究预览（limited research preview）」。边界也由发布方自己划定：工具今天只支持 Rust，证明覆盖不到的场合并不给出硬保证。
演示的主会场在旧金山 Fort Mason Center，大会官网显示线上虚拟参加免费（）；GitHub Next 在公告里招呼大家「到 Speakeasy 找 GitHub Next」，Lavaee 则表示他会在大会上分享 PDD Kit，聊「经过验证的代码」。
而在发布帖的回复区，用户 Lachy 留下了一个尚无回复的问题：「如果形式化规范由 AI 起草、由我批准，什么机制能发现一个『有效、但悄悄弱于我的本意』的规范？」（）Lavaee 在帖文里主张 PDD Kit「不仅证明代码正确，也证明你的意图」；但证明只对写进规范的承诺负责——当整个流程把人的判断推到最上游的那份规范上，规范是否完整表达了意图，就成了留给使用者自己的问题。