Microsoft Research· Alex Lavaee, Matthai Philipose·· 4 小时前精选AI 评分65
微软研究院发布 PDD Kit：用形式化验证保障智能体编写的代码
Formally verifying agent-written full-stack web apps with PDD Kit
AI 导读
微软研究院联合 GitHub Next 推出研究原型 PDD Kit，旨在通过形式化验证确保编码智能体严格遵循用户设计意图。该工具引入证明驱动开发（PDD）范式，将自然语言需求转化为 Rust 证明语言 Verus 的形式化规范，由智能体生成代码及数学证明，并通过 Verus 和 Z3 求解器对所有可能输入完成确定性机器验证。
推荐理由
针对编码智能体生成海量代码难以逐行审查的问题，该工具将审查重心转移到自然语言意图与形式化规范上，为解决生成代码漂移提供了可落地的工程范式。
来源：Microsoft Research · microsoft.com