Verus

微软PDD Kit用形式化证明核验智能体代码

微软研究院11月5日介绍了PDD Kit：它与开发者一起把开发意图转成Verus形式化规格，再证明AI编程智能体生成的代码对所有输入都符合该规格；证明无法覆盖的部分则使用测试。 这项工具针对的是“计划与实现不一致”的问题。微软研究院指出，智能体可能实现了与要求略有不同的功能，再编写能通过自身实现的测试。当生成代码越来越多时，逐行人工审查难以扩展，测试通过也不等于代码实现了开发者原本的意图。