Microsoft Research 发布 PDD Kit

Microsoft Research 推出了 Proof-Driven Development Kit，旨在通过将自然语言开发者意图转化为 Verus 规范，利用形式化验证中的数学证明来测试智能体生成的代码并提高其可靠性。该套件将传统用于安全关键系统的形式化方法引入 AI 编码，能够标明证明无法触及的范围，帮助开发者应对代码规模过大而难以逐行审查的信任问题。

Microsoft Research 发布 PDD Kit 工具包，引入证明驱动开发（PDD）新范式，结合 GitHub Next 的 Chopin 环境与 Verus 形式化验证工具，将用户的自然语言意图转化为数学规范。该工具包通过自动生成代码证明和受信任的测试边界，在全栈 Rust 应用的登录逻辑验证中实现对每个输入的穷举式证明，从而减少对代码逐行审查的依赖。