微软研究院放出 PDD Kit 工具，用来对 AI 智能体 Agent 写出来的代码做形式化证明，靠 Verus 验证框架校验代码逻辑是否符合预设规范，测试案例选用了约 5000 行 Rust 编写的商城应用，优先验证登录这类关键模块，不过微软自己直接写明这套方案存在四个硬性限制，说明它不是能直接全量落地的通用工具，现阶段更适合用来保障高风险小内核代码，不能直接给整个大仓库做验证。现在很多编码 Agent 会一次性输出大量代码，虽然能跑通简单测试，但隐藏逻辑漏洞、权限漏洞，普通单元测试很难覆盖所有边界，形式化证明可以从数学层面确认代码满足安全规范，微软推出这套工具就是想解决 Agent 代码不可控、行为不可预期的痛点，但是受技术、成本、语言约束，适用场景被明显收窄。
PDD Kit 基础信息清单
- 工具名称：PDD Kit
- 底层依赖：Verus 形式化验证框架
- 核心能力：对 Agent 产出的代码做形式化证明，校验代码是否匹配规范
- 测试 Demo：Rust 语言商城应用，代码规模约 5000 行，优先验证登录模块
- 核心思路：证明驱动开发，把计划作为智能体和代码之间的约束契约
- 定位：研究原型工具，面向高安全需求的小型代码模块
微软官方标注的四大限制清单
- 仅支持 Rust 语言：PDD Kit 依托 Verus，只能验证 Rust 代码；其他语言代码只能移植到 Rust 或者通过调用已验证 Rust 包间接使用
- 属于研究原型：还没有达到工业级稳定产品状态，不适合直接大规模上线用于生产项目
- 证明过程需要投入成本：写规范、跑证明都要耗费时间，小模块几秒完成，规模偏大的代码可能要数分钟，不适合随便拿来验证所有代码
- 规范本身也可能出错：形式化证明只能证明代码满足写好的规范，没法保证规范本身和真实业务需求一致，规范写错，证明结果再正确也没有意义
PDD Kit 使用落地步骤
- 选定高风险模块，优先选择登录、鉴权这类边界清晰、体量小的代码，不适合大业务模块
- 使用 Rust 开发，基于 Verus 编写对应的形式化规范，把业务需求翻译成可验证规则
- 调用 PDD Kit，对 Agent 生成的 Rust 代码执行形式化证明
- 人工评审规范，确认规范和原始业务意图一致，规避规范写错的问题
- 结合普通测试、代码评审一起使用，用形式化证明补充传统测试的短板
整体来看，PDD Kit 是提升 Agent 代码可靠性的补充手段，并不是用来替代测试、代码评审的万能方案，四大限制直接划定了它的使用边界，后续想大范围落地，还需要解决语言兼容、验证耗时、规范编写难度这些问题。
【常见问题】
问题 1：微软研究院推出 PDD Kit 给 Agent 代码做形式化证明，这四个限制分别是什么？
回答 1：微软研究院推出 PDD Kit 给 Agent 代码做形式化证明，四个限制分别是仅支持 Rust、属于研究原型、证明需要投入成本、规范本身存在写错的可能性。
问题 2：微软研究院推出 PDD Kit 给 Agent 代码做形式化证明，这个工具是用来完全替代单元测试吗？
回答 2：微软研究院推出 PDD Kit 给 Agent 代码做形式化证明，它不能替代单元测试，只是补充手段，适合给登录等高风险小模块做逻辑校验，需要搭配常规测试和代码评审一起使用。
问题 3：微软研究院推出 PDD Kit 给 Agent 代码做形式化证明，非 Rust 语言写的 Agent 代码能不能用这套工具？
回答 3：微软研究院推出 PDD Kit 给 Agent 代码做形式化证明，原生只支持 Rust，其他语言代码需要移植到 Rust，或者调用已经验证好的 Rust 包间接使用。
【参考资料】
[2026-11-11]（微软研究院给 Agent 的代码做证明，然后自己写了四个限制）博客园
[2026-11-11]（微软研究院给 Agent 的代码做证明，然后自己写了四个限制）DevPress
[2026-11-05]（Formally verifying agent-written full-stack web apps with PDD Kit）微软研究院官网
[2026-11-06]（Microsoft Research Launches PDD Kit to Formally Verify Agent-Written Code）ClawdBytes
【免责声明】
本文仅为公开技术资讯整理，PDD Kit 属于研究原型工具，验证效果、适用范围以微软研究院官方文档为准，不构成企业代码安全方案选型建议，形式化证明不能完全消除代码风险。