Microsoft Research· Alex Lavaee, Matthai Philipose·· 5 小时前AI 评分55
微软研究院用 PDD Kit 形式化验证智能体编写的全栈 Web 应用登录逻辑
Formally verifying agent-written full-stack web apps with PDD Kit
AI 导读
微软研究院与 GitHub Next 展示 PDD Kit：先把开发者意图转成 Verus 形式化规约，再证明智能体生成的代码对每个输入都满足规约，证明覆盖不到的信任边界才交给测试。在约 5000 行 Rust 的 Pet Store 上，团队用它验证登录逻辑并发现既有 bug，开发者只审阅意图文档而未逐行阅读生成代码。PDD Kit 目前是研究原型，只支持 Rust。
来源：Microsoft Research · microsoft.com