Microsoft Research 用 PDD Kit 形式化验证 Agent 编写的全栈 Web 应用登录逻辑

Microsoft Research 与 GitHub Next 合作推出 PDD Kit，将开发者的自然语言意图转成 Verus 形式化规范，用数学证明约束编码 Agent 生成的代码对每个输入都符合规范，证明覆盖不到的部分回退为测试。