微软研究院发布 PDD Kit，用 Verus 形式化验证智能体编写的全栈 Web 应用

微软研究院联合 GitHub Next 发布研究原型 PDD Kit，把用户意图转成 Verus 形式化规范，证明智能体生成的代码对每个输入都满足规范，证明覆盖不到的部分改用测试。团队在 GitHub Next 的 Chopin 环境中用它验证了 Rust 全栈应用 Pet Store 的登录逻辑，开发者只审查意图文档而未逐行阅读生成代码，登录处理器的六个受信任组件由测试覆盖。