微软发布 PDD Kit：形式化验证智能体生成的全栈 Web 应用
原标题：Formally verifying agent-written full-stack web apps with PDD Kit
AI 摘要
微软研究院发布 PDD Kit，将形式化方法引入日常软件开发：它把用户意图转化为 Verus 形式化规范，证明编码智能体生成的代码对所有输入都满足规范，无法证明的部分则回退到测试。团队在 GitHub Next 的 Chopin 环境中用其验证 Rust 全栈网店 Pet Store 的登录逻辑，证明不存在登录缺陷并发现既有 bug，开发者无需逐行阅读生成代码。
正文节选
At a glance - Formal methods for everyday software. PDD Kit helps you turn your intent into a formal spec, then proves the code your agent writes for every input and uses tests where a proof can’t reach. It takes formal methods beyond niche, specialist work to engineers without a formal methods background and to everyday applications, like the full-stack web app shown here. - Exhaustive line-by-line human review can become difficult to scale as AI agents generate increasingly large amounts of co