Microsoft Research 介绍用 Proof-Driven Development Kit 解决 AI 生成代码的信任问题

Microsoft Research 介绍 Proof-Driven Development Kit，用于解决 AI 智能体生成代码难以逐行审查的信任问题。该工具把开发者的自然语言意图转成 Verus 规范，沿用安全关键系统中的形式化方法，用数学证明尽可能验证智能体生成的代码是否符合规范，并明确标出证明无法覆盖的部分。研究人员在 MSR 博客中详细拆解了这一方法。