微软 PDD Kit 如何用形式化验证约束智能体生成的全栈 Web 应用

微软研究院推出 PDD Kit，把用户意图转成 Verus 形式化规范，证明智能体生成的代码对所有输入都满足规范，证明覆盖不到的部分则回退到测试。团队在 GitHub Next 的 Chopin 中用它对 Rust 商店应用 Pet Store 的登录逻辑做形式化验证，Verus 加固了代码并发现既有 bug，开发者只审阅意图、未逐行阅读生成代码。