Microsoft Research· Alex Lavaee, Matthai Philipose·· 4 小时前精选
微软研究院发布 PDD Kit，以形式化验证提升 AI 代理编写全栈 Web 应用的可信度
Formally verifying agent-written full-stack web apps with PDD Kit
原始来源：Microsoft Research阅读原始报道
AI 导读
微软研究院发布 PDD Kit（证明驱动开发工具包），帮助开发者把意图转化为 Verus 形式化规范，并证明 AI 代理生成的代码对每个输入都满足规范，无法证明的部分回退到测试。团队在 GitHub Next 的 Chopin 环境中，对约 5000 行 Rust 编写的全栈宠物商店应用的登录逻辑进行了形式验证，发现并修复了现有登录漏洞，开发者无需逐行审阅生成代码。
推荐理由
该工具直击 AI 代码生成难以逐行审查的痛点，把形式化验证与测试结合为“证明驱动开发”，对提升 AI 编程代码可信度有参考价值，但目前仍是研究原型且仅支持 Rust。
来源：Microsoft Research · microsoft.com
新闻讨论
读者观点通过 GitHub Discussions 发布，发言需登录 GitHub；评论不等于已经核实的事实。
在 GitHub 打开讨论