微软研究院发布 PDD Kit，用 Verus 形式化验证智能体生成的代码
Formally verifying agent-written full-stack web apps with PDD Kit
微软研究院联合 GitHub Next 发布研究原型 PDD Kit，将开发者的自然语言意图转为 Verus 形式化规格，再证明智能体生成的代码满足该规格，证明无法覆盖的部分改用测试。团队在约 5000 行 Rust 编写的全栈应用 Pet Store 上验证了登录逻辑，开发者只审查意图与规格，未逐行阅读生成代码。PDD Kit 目前仅支持 Rust。
这条信号在站内保留事实摘要与战略研判。完整内容和上下文请以原文为准；融资、并购与技术效果以原始披露为准。
战略研判
基于公开信息PDD Kit 把审查对象从逐行代码转向自然语言意图与形式化规格，若在 Rust 项目中可用，可能降低智能体生成大规模代码后的审查成本，但保证强度受限于六个被信任的外部组件。
Pet Store 登录之外的功能能否同样完成证明；Verus 证明在更大代码库中的耗时与维护成本。
AI agents can generate code at a scale that’s hard for humans to review line-by-line. PDD Kit helps ensure the code is doing what the developer intended by creating formal specifications and testing against them. It converts developer intent into a Verus specification, proves AI-generated code meets it for every input, and uses tests where proofs aren't practical. Developers review intent, not every line. The post Formally verifying agent-written full-stack web apps with PDD Kit appeared first on Microsoft Research .
来源只提供摘要，完整内容请打开原文。
来源：Microsoft Research · microsoft.com