使用 PDD Kit 形式化验证全栈网络应用

PDD Kit 帮助将意图转化为形式化规范，并证明代理为每个输入编写的代码符合该规范，同时使用测试来补充证明无法覆盖的部分。 它将形式化方法扩展到没有形式化方法背景的工程师和日常应用程序，如全栈网络应用程序。 随着 AI 代理生成越来越多的代码，彻底的逐行人工审查可能难以扩展。 PDD Kit 与您合作，将您的意图转化为 Verus 中的形式化规范，证明代理的代码符合该规范，并在证明无法覆盖时回退到测试。

在 GitHub Next 的 Chopin 中，我们使用 PDD Kit 对 Rust 店铺 Pet Store 的登录逻辑进行了形式化验证。 Verus 加固了代码并发现了现有错误，证明了相对于规范的登录错误不存在。 开发者审查了意图，从未逐行阅读生成的代码。 计划是代理应该遵循的合同，但没有任何东西约束代理遵循它。 现在，编码代理通常一次性交付整个功能，往往跨越数万或数十万行代码。 因此，阅读每个 pull 请求的行不适用于这种新工作方式。

现在，大多数团队投资于计划和相关测试：向代理描述他们想要什么，来回讨论直到计划和提出的测试看起来正确，然后将它们交给代理进行实现。 这个计划或自然语言规范是代理应该持有的合同。 然而，在实践中，代理可能会偏离它。 它实现了一些略有不同的事情，然后编写了通过其实现而不是您打算编写的代码的测试。 由于低质量和大量测试的泛滥，持续集成 (CI) 在增长，覆盖率看起来很健康，您要求的东西和交付的东西之间的差距直到出现错误报告或恶劣的边缘情况才会显现。 那么，当代理生成越来越多的代码时，如何可靠地扩展审查？

代理代码失败的两种方式是仔细的审查者通常会捕获的：它遗漏了明显必要的东西，或者它做了明显错误的事情。 测试本身无法弥补这个差距，因为它们只执行了程序可以做的事情的一小部分。 弥补它需要不同类型的机制，这就是证明的作用所在。 审查询问“这个看起来对吗？ ”证明回答“这个是对的吗？ ”数学证明表明代码对于每个输入都符合其规范，包括测试套件可能遗漏的输入。 这比单独测试提供了更强的指定属性保证，尤其是在逐行审查不实用时。 证明过去对日常软件来说太昂贵了。

您需要专家、不熟悉的语言、比代码大得多的证明，并且证明需要花费数年才能开发，但有两件事自那以来发生了变化。 首先，最近的编码代理进步使它们越来越实际地从定义良好的规范中生成形式化证明。 其次，代理现在可以更好地帮助您编写形式化规范。 我们称之为新的软件开发范例“证明驱动开发”（PDD）。 PDD Kit 是我们为此目的的工具包。 PDD Kit 的工作原理 PDD Kit 对于形式化方法大致相当于 Spec Kit 对于 Spec-Driven Development。

它作为 Chopin（GitHub Next 的实时、多人规划环境）内部的合作伙伴运行，团队和代理可以在一个共享文档中规划。