用 PDD Kit 形式化验证智能体编写的全栈 Web 应用

判断

使用编码智能体的工程负责人必须先决定是否对高风险路径要求 Verus 规约，并接受编写规约的成本，再允许智能体代码绕过逐行评审。

依据

Microsoft Research 的 Alex Lavaee 和 Matthai Philipose 表示，PDD Kit 将意图转为 Verus 形式化规约，证明智能体代码对每个输入都满足该规约，并在证明无法覆盖处回退到测试。在 GitHub Next 的 Chopin 中，他们将其应用于 Pet Store 的登录逻辑：Verus 发现了既有缺陷，并证明了相对于该规约不存在登录缺陷，而开发者评审的是意图，从未逐行阅读生成的代码。这使规约而非逐行评审成为评审产物，但团队必须在智能体可交付数万或数十万行代码的同时，承担编写和维护 Verus 规约的成本。