证明驱动开发：agent 能证明自己的代码真的能跑吗？
用 agent 写代码有个麻烦：你可以让它实现功能、补上测试、把全部流程跑一遍，再让它解释为什么这样做是对的——结果代码里还是有 bug。你可以再找另一个 agent 来审查，这确实有点用，但审查结论本身是否靠谱，又得再验证一遍。如今生成代码变得极其容易，我们反而要头疼怎么跟上检查的速度。对着同一个大语言模型（LLM）反复追问“你确定吗？”，其实给不了多少保障。
所以 GitHub Next 的这则公告让我很感兴趣。微软研究院正在开发 Proof Driven Development Kit（简称 PDD Kit），把形式验证（用数学方法证明程序满足特定性质）引入 agent 的开发流程。思路是：要求 agent 给出一个数学证明，说明实现满足规范，再交给独立的验证器检查这个证明。我觉得有意思的地方在于，正确性论证必须经受比“agent 自己解释为什么代码没问题”更严格的检验。
GitHub Next (@GitHubNext) 在 X 上
好吧，它到底在做什么？
根据公告，PDD Kit 会和你讨论代码，弄清楚你想实现的目标，然后提出一份形式化规约（formal specification）。你审阅并批准这份规约后，实现代码会被拿去用 Verus 检查是否与规约一致——Verus 是一个针对 Rust 的验证工具。演示展示了一条登录流程，从最初的意图一直到生成经过验证的拉取请求。它还能和 Chopin 集成，这是 GitHub Next 的协作规划环境，团队可以一起把方案过一遍。在无法进行形式化证明的地方，工作流会用测试和 computer-use agent 来检查行为。目前公布的语言支持是 Rust，Verus 在 Rust 代码周围添加了规约和证明的语法。
我觉得好的一点是：有 LLM 之外的东西在检查这个形式化声明。agent 可以提出实现，但它不能因为解释听起来有道理就自己宣布作业做对了。Verus 文档把这种做法的叫作静态验证：检查代码是否在模型覆盖的所有执行路径上都满足指定属性，不添加运行时检查。想想我们花了多少时间担心有没有漏掉某个该测的输入。对于能这样表达并验证的属性，这个保证要强得多。但这一切里有个非常重要的词：规约。
这里才是关键问题所在
假设你在实现会话校验。你希望持有有效会话的用户能访问应用，其他人一律拒绝。你让 agent 实现这个检查，它给了你类似这样的东西。我用 JavaScript 来举例，方便大家理解；PDD Kit 目前公布的形式化验证支持是给 Rust 用的。
function canUseSession(session, now) {
return session.signatureValid && now < session.expiresAt;
}
看起来没问题。签名有效，会话也没过期。你测试了有效会话、过期会话和无效签名，全部通过。然后用户登出，你把会话标记为已撤销，结果……这个函数仍然接受它。我们根本没检查 session.revoked。可以为此补一个测试，也应该补。但现在想象一下，我们此前把这个函数正式规定为：当且仅当签名有效且会话未过期时接受该会话。 实现满足这条规则。我们可以证明它，却仍然带着完全相同的 bug，因为我们在需求里也忘了撤销。
这正是 Chopin 和 PDD Kit 想要帮我们抓住的那类缺口。PDD Kit 会先讨论预期行为，再提出形式化规格，而 Chopin 给团队一个共享场所来质疑计划并敲定这些决策。对这个例子来说，那场讨论应该包括：“登出会立即撤销会话吗？”、“在正好过期的时刻会发生什么？”以及“每个在其他方面有效的会话都应该被接受吗？”这些工具可以帮忙把“让会话验证能工作”变成一组明确的决策，并把答案带入规格中。这是工作流中有用的一部分：你不必一开始就拿出完美的规格。
把这些问题过一遍之后，规则可以写成：当且仅当会话签名有效、未被撤销，且当前时间严格早于过期时间时，才接受该会话。 这样过期边界就定了：正好处在过期时刻时访问应被拒绝，所以用 <= 的实现会违反规格。“当且仅当”还要求有效会话必须被接受——少了这一点，一个对所有人都返回 false 的实现，也能满足一条只要求“拒绝无效会话”的更窄规则。恭喜，结果是谁都登不进去了。这就是为什么讨论要和证明放在一起：工具帮我们理清自己到底想表达什么，验证再检查实现是否符合我们达成的共识。工具仍可能漏掉某个需求，但帮我们把这些需求挖出来，本身就是它们的价值所在。
完全按计划建造。却还是没法让你过河。
管理员，但谁的管理员？
如果要做一个超出微软登录演示范畴的应用，我想在租户权限上试试这套流程。设想你在做一个 SaaS 应用，管理员可以删除文档。智能体会检查用户是不是活跃管理员，测试里一切看着都没问题——因为测试夹具里的每个用户和文档都属于同一家公司。然后有人传入了一个另一家公司的文档 ID，结果发现“当管理员”似乎成了一种全球通用的成就。糟了。这条规则必须把用户的成员关系跟文档所属的租户关联起来。用 Verus 语法写一个简化版后置条件，大致如下（假设这些值在函数里已经能取到）：
ensures
allowed == (
active_member
&& is_admin
&& member_tenant == document_tenant
),
这里我希望 agent 考虑四种情况：正确租户里的活跃管理员、另一个租户里的活跃管理员、不活跃管理员，以及普通成员。第二种情况最值得关注：角色本身有效，但关系错了。针对这个契约的证明必须覆盖不同的租户 ID，而不只是某人碰巧塞进测试里的公司 ID。我们还需要确认，应用确实提供了实际的文档租户和正确的成员记录。如果它对两个参数都传了用户的租户 ID，决策可以完美遵循这条规则，但应用照样会泄露访问权限。
总得有人知道该问什么
我之前说过：你无法提示自己不知道存在的东西。如果你不知道会话可以被撤销，很可能就不会注意到规范里缺了撤销功能。这也是一个研究问题。微软研究院把从非正式需求到可检验规范的转换称为意图形式化。Shuvendu Lahiri 的文章指出，验证这些规范是核心瓶颈。仍然需要有人确认：形式化陈述是否与用户的真实意图相符。
我们的会话示例里还有一个细节：signatureValid 是一个输入，函数并不验证签名。now 也一样：我们给它一个时间戳，它就信任这个值。对这个决策的证明，并不能确立密码学正确、时钟准确，或者每个受保护端点真的调用了这个函数。这些都需要各自的保证或检查。所以当一个 PR 说“已验证”时，我想知道验证了什么。会话决策？HTTP 处理器？整个登录流程？哪些部分被证明、被测试、被假设了？这正是 PDD Kit 把形式化验证和经验性验证结合起来的意义所在。你可以证明一个决策遵循规则，同时用集成测试检查应用是否提供了正确的输入、是否在正确的位置调用了它。
证明只覆盖边界以内的部分。输入仍然得从外面来。
我会如何把它用到 JavaScript 上
我不写 Rust，所以 Verus 没法直接用在 JavaScript 项目里。不过我可以借鉴 PDD Kit 的思路：先就契约达成一致，再让 agent 生成实现。我会用 Chopin 来共享计划、问题和决策，再通过它的 MCP server 连上编码 agent。然后把商定好的规则转成单元测试和集成测试，用 fast-check 跑各种生成的输入组合，再给用户流程补上浏览器端检查。拿前面说的会话例子来说，就是要明确检查：撤销是否生效、过期边界怎么处理、有效会话是否被放行。这样虽然给不了 JavaScript 同样的形式化保证，但能让 agent 拿到具体的需求去实现，也让我们在合并前有明确的点可查。
在 Rocket.Chat，我们已经在明显提升代码覆盖率，每个新功能都必须配足够的测试。PDD 的思路或许能帮我们把这份投入用得更值：在写测试之前先把预期行为讲清楚。 比如要改房间权限，agent 可以陪我们理清谁该有访问权、谁不该有、成员变动时又会怎样。这些商定好的规则，在评审时能直接对上实现和测试，缺失的用例也更容易被发现。