Microsoft Research 发布 PDD Kit 用形式化证明验证 Agent 生成的 Rust 全栈应用

Microsoft Research 与 GitHub Next 合作推出 Proof-Driven Development (PDD) Kit，旨在解决 AI Agent 生成大规模代码时人工逐行审查无法扩展的问题。该工具将开发者的自然语言意图转化为 Verus 形式化规范，利用 Verus 证明器自动验证 Agent 生成的代码是否满足规范，并在证明不可达处使用测试补充。在 Pet Store 全栈应用的登录逻辑验证中，开发者仅需审查意图文档而非数万行代码，即可确保核心逻辑的正确性。

PDD Kit 的核心机制在于明确区分“证明”与“信任”。对于 Verus 可覆盖的逻辑（如密码比对、Token 签发），系统生成数学证明；对于外部依赖（如 bcrypt 哈希、SQLite 查询、时钟读取），则标记为可信计算基（TCB）并辅以测试。例如，登录流程中的数据库查找和哈希验证被封装为带有假设契约的外部函数，开发者需手动确认这些假设，随后系统自动生成针对这些假设的 Given/When/Then 场景测试。这种设计避免了传统测试仅覆盖部分输入路径的盲区，同时通过变异检查（mutation check）防止模型生成弱不变量导致的“氛围验证”。

事实层面，PDD Kit 目前仅支持 Rust 语言，依托 Verus 证明器和 Z3 求解器运行，Pet Store 案例涉及约 5,000 行 Rust 代码。推断层面，该工具标志着软件工程从“测试驱动”向“证明驱动”的范式迁移，将审查重心从实现细节转移至需求定义。猜测层面，随着外部库契约的逐步完善，可信边界有望缩小，但短期内仍需依赖人工确认 TCB 假设。这要求团队在引入 AI 编码时，必须建立更严谨的需求规格定义能力，而非单纯依赖代码生成速度。