Microsoft Research 推出 PDD Kit，用 Verus 形式化验证智能体编写的全栈 Web 应用

Microsoft Research 联合 GitHub Next 提出 Proof-Driven Development（PDD）范式并发布研究原型 PDD Kit，在 Chopin 规划环境中把开发意图转化为 Verus 形式化规范，用数学证明验证智能体编写的 Rust 代码对每个输入满足规范，证明覆盖不到处回退为测试并标注证据边界。