微软提出Proof-Driven Development，用形式化证明验证AI智能体生成的全栈应用

作者 Alex Lavaee 研究软件工程师 Matthai Philipose 高级首席研究员

这份计划或自然语言规格说明，本应成为 agent 所遵循的契约。然而在实践中，agent 可能会偏离它。它实现了略有不同的东西，然后编写能为其实现通过的测试，而不是你原本希望它编写的代码。持续集成（CI）因大量低质量、高数量的测试而不断膨胀，覆盖率看起来健康，而你要求的和实际交付之间的差距一直隐藏着，直到出现缺陷报告或棘手的边缘情况才暴露出来。

那么，当 agent 生成越来越多的代码时，如何可靠地扩展审查？Agent 代码会以两种方式失败，而细心的审查者通常能抓住：它遗漏了某些明显必要的东西，或者它做了某些明显错误的事情。仅靠测试无法弥合这一差距，因为测试只覆盖了程序可能行为的一小部分。弥合这一差距需要一种不同的机制，这就是证明的用武之地。

了解 Microsoft 如何从其他领域学习，以推进评估和测试作为 AI 治理的支柱。

审查问的是“这看起来对吗？”证明回答的是“这是对的吗？”数学证明表明代码对其规格对于每个输入都成立，包括测试套件可能遗漏的输入。对于已指定的属性，这提供了比仅靠测试更强的保证，尤其是在逐行审查不切实际的情况下。

证明过去对于日常软件来说过于昂贵。你需要专家、不熟悉的语言、比代码大许多倍的证明，而且证明需要数年时间才能开发出来，但此后有两件事发生了变化。首先，编码 agent 的近期进展使得它们从定义良好的规格生成形式证明变得越来越实用。其次，agent 现在能更好地帮助你编写形式规格。我们将这种新的软件开发范式称为证明驱动开发（PDD）。PDD Kit 是我们为此提供的工具包。

PDD Kit 之于形式化方法，大致相当于 Spec Kit（在新标签页中打开）之于规格驱动开发。它作为 Chopin（在新标签页中打开）内的合作伙伴运行，Chopin 是 GitHub Next 的实时、多人规划环境，团队和 agent 可以在一个共享文档中共同规划。

工作流程分为两半（图 1）。首先，团队成员用平实的语言审查意图。PDD Kit 会提出细心的审查者会提出的问题，在过程中解释相关代码，并将答案记录在意图工件中——这是一份连接用户意图与形式规格或测试的文档。用户意图中可形式化的部分被转换为形式规格，其余必须被信任的部分被转换为非形式规格用于测试。PDD Kit 自动生成证明，证明代码满足导出的形式规格，并为非形式规格生成高质量测试。你不需要具备形式化方法背景就能完成这一切。

因此，PDD Kit 中的每个结果都会说明它基于哪种验证：

两者之间的界线是可信计算基（TCB）：证明假定其行为如所述的代码。PDD Kit 明确标出这条界线，并要求你逐项签字确认。

为了展示 PDD Kit 与现有代码库的集成，我们构建了 Pet Store，一个完全用 Rust 编写的全栈 Web 应用（在新标签页中打开）。后端使用 Axum（在新标签页中打开）和 SQLite（在新标签页中打开），处理库存、促销、订单和结账。店面是一个编译为 WebAssembly（在新标签页中打开）的 Leptos（在新标签页中打开）应用。它们合计约 5,000 行 Rust 代码。

为简洁起见，本文重点对应用的登录逻辑进行形式验证，但同样的流程可用于验证整个应用的功能正确性。PDD Kit 建议从应用中最敏感的部分开始，逐步验证你的应用。登录缺陷可能让攻击者获得客户账户或管理员的控制权，因此证明工作应首先在这里见效。开发者在 Chopin 中的整个请求只有两句话：

验证 backend/src/handlers/auth.rs 中的登录逻辑。以下是我的需求：

我们故意让请求保持粗略。捕获用户意图并将用户请求转化为证明可检查的内容，是 PDD Kit 的职责。

PDD Kit 的规划工作流 pdd-plan 读取代码，并在写任何东西之前，在 Decisions 标签页中带着问题返回。当问题取决于代码如何工作时，卡片会先解释那部分：目标、各部分如何组合，以及涉及的确切函数，这样你无需打开源代码就能回答。

这个问题看起来迂腐，但很重要。“只有密码正确才能获得 token”排除了坏情况——错误密码获得 token，而拒绝所有人的登录完美地遵守了这一承诺。“正确密码始终有效”是排除该情况的那一半。形式上，第一个是蕴含（token ⇒ 正确密码），第二个是它的逆命题。两者合在一起构成“当且仅当”。放任不管的 agent 会不告诉你就选一个，但在这里开发者两个方向都选了。

随着对话继续，PDD Kit 会在计划顶部维护一个粗略的工作区，以便用户跟踪重要概念，而不必在长长的聊天记录中往回滚动查找已达成一致的内容。它包括正在规格化的登录流程图、将要证明什么和信任什么的规定全景图，以及在图片有帮助时的思维模型。对于登录，PDD Kit 画了一个票务柜台（图 3）。

在它下方，意图图将每项需求追溯到开发者自己的话，并记录它是如何确定的（图 4）。每个条目链接到对其进行建模的形式规格部分以及覆盖它的测试，规格部分显示 Verus 合约的片段，并带有注释，以便开发者看到形式规格如何对其意图建模。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）