微软推出 PDD Kit：用形式化证明保证 AI 生成代码正确性

omojumiller · x · 2026-10-22

问题：Agent 写的代码已多到人类无法逐行审查，现有 review 最多只能粗读 diff。研究显示最好的 AI 代码审查员首轮就抓到 bug 的比例仅 42%，评估瓶颈、回归与安全事件频发。
方案：微软研究院发布 Proof-Driven Development Kit（PDD Kit），把你在自然语言中描述的目标固化为「意图」，再用 Verus（Rust 证明语言）生成形式化规范，由验证器对所有可能输入证明代码符合规范。
工作流：你只审阅计划和目标（自然语言），不看代码也不看证明；无法证明的部分回退到经验性验证。已与 GitHub Next 的 Chopin 集成，支持团队协作规划，官方示例演示了从登录流程意图到已验证 PR 的全过程。

「编程与Agent」频道最新