Microsoft Research· Alex Lavaee, Matthai Philipose·· 3 小时前精选AI 评分72
微软发布 PDD Kit 用形式化验证 Agent 编写的完整栈 Web 应用
Formally verifying agent-written full-stack web apps with PDD Kit
AI 导读
微软研究发布 PDD Kit，把开发者意图转成 Verus 形式化规格，再证明 Agent 写的代码对每个输入都满足该规格，证明达不到的地方回退到测试。它在 GitHub Next 的 Chopin 中验证了 Rust 电商应用 Pet Store 的登录逻辑，硬化代码并发现既有 bug，证明其不存在登录漏洞。
推荐理由
微软给出形式化验证从意图到证明的完整工作流，可据此判断它如何改变 AI 生成代码的审查方式。
来源：Microsoft Research · microsoft.com