微软研究院发布 PDD Kit 以形式化证明保障 AI 生成代码正确性

微软研究院发布 Proof-Driven Development Kit（PDD Kit），可利用 Verus 生成形式化规范，并由验证器证明代码对所有可能输入符合规范。用户只需审阅自然语言计划和目标，无法证明的部分回退到经验性验证；该工具已与 GitHub Next 的 Chopin 集成，官方示例展示了从登录流程意图到已验证 PR 的全过程。