Microsoft Research 发布 PDD Kit，可形式化验证 AI 代理编写的全栈 Web 应用

Techub News 消息，Microsoft Research 发布 PDD Kit 工具包，旨在通过形式化验证确保 AI 代理编写的代码符合开发者意图。该工具可将开发者的意图转化为 Verus 形式化规范，并证明 AI 代理生成的代码在所有输入下均满足该规范，对于无法证明的部分则回退到测试。 在 GitHub Next 的 Chopin 项目中，研究人员使用 PDD Kit 对名为 Pet Store 的 Rust 商店应用的前端登录逻辑进行了形式化验证，验证过程强化了代码并发现了既有错误，最终证明了代码在规范下不存在登录漏洞。开发者只需审查意图，无需逐行阅读生成的代码。