证明驱动开发：agent 能证明自己的代码真的能跑吗？

用 agent 写代码有个麻烦：你可以让它实现功能、补上测试、把全部流程跑一遍，再让它解释为什么这样做是对的——结果代码里还是有 bug。你可以再找另一个 agent 来审查，这确实有点用，但审查结论本身是否靠谱，又得再验证一遍。如今生成代码变得极其容易，我们反而要头疼怎么跟上检查的速度。对着同一个大语言模型（LLM）反复追问“你确定吗？”，其实给不了多少保障。 所以 GitHub Next 的 这则公告 让我很感兴趣。微软研究院正在开发 Proof Driven Development Kit （简称 PDD Kit），把形式验证（用数学方法证明程序满足特定性质）引入 agent 的开发流程