微软研究院推出 PDD Kit 校验 AI 代码

微软研究院介绍 Proof-Driven Development（PDD）Kit：先将开发者意图转译为形式化规格，再用形式化验证证明生成的代码符合该规格，以应对 AI 智能体编写越来越多代码带来的正确性问题。 该工具面向 Rust，与验证工具 Verus 配合使用，并集成到 GitHub Next 的 Chopin 中，将形式化方法引入 AI 辅助开发流程。上述定位来自微软研究院的说明，尚未见对实际效果的独立验证。

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。