微软研究院展示 PDD Kit，用 Verus 证明 AI 写的 Rust 登录逻辑

微软研究院与 GitHub Next 展示 PDD Kit，把开发者意图转成 Verus 规格并证明代码，在约 5000 行 Rust 的 Pet Store 上验证登录逻辑，目前仅支持 Rust。