Claude 写 Dafny 证明不再逐条硬推：37 个算法机器校验通过，三连通性测试也在其中
核心概要
埃因霍温理工大学团队把大语言模型辅助的 Dafny 形式验证组织成十步工作流，由 Claude Code 担任验证构建智能体，在人工监督下完成规格、实现、不变式与证明。该流程在 37 个图论、标记迁移系统和计算几何算法上得到机器校验的 Dafny 实现，其中包括 Hopcroft–Tarjan 三连通性测试；作者称许多验证在数小时到数天内完成，但未与人工主导的验证做对照。
深度剖析
形式验证的瓶颈从写出数学论证转向让证明检查器能处理证明，大语言模型被放进一条有固定步骤和人工把关的流程里承担这部分工程工作。 此前大语言模型在 Dafny 上的应用多集中在引理生成、标注合成或循环不变式生成等单项任务，或假定已有实现再补证明。 这条流程覆盖从文献中的算法描述出发，到规格、实现、不变式、证明和验证优化的完整开发过程，并在 37 个算法上产出机器校验的 Dafny 实现。
流程把验证拆成规格、代码生成与契约测试、证明开发三大阶段，每一步都有明确的输入、输出和完成标准。 规格阶段先由智能体把论文算法转写成伪代码并形式化为前后置条件组成的前置契约，经人工审阅后锁定，之后不得在未经批准时改动。 在证明阶段，智能体先在资源受限的子智能体循环中单独验证每条证明义务，再迭代到整个文件在 Dafny 原生配置下通过验证，并用工具审计是否存在未加证明的假设。
求解器资源测量被用来指导证明重构，而不只是判断证明对错。 Lengauer–Tarjan 支配点算法的主验证例程原先有 644 条证明义务并出现 36 次超时，Z3 资源消耗约 21 亿单位。 把契约和不变式藏到不透明谓词之后、再用显式引理按需揭示事实后，义务数降到 271，超时全部消除，资源消耗降到 1.44 亿单位。
启示与展望
演示范围是文献中已发表、以伪代码给出的算法，覆盖图论、标记迁移系统和计算几何共 37 个目标，验证在 Dafny 4.10.0 与其自带 Z3 上完成，单次运行限制为六核和 12 GB 内存；低层实现细节、内存管理和语言相关优化不在范围内。
作者指出所选算法多为知名且可能出现在当代大语言模型训练数据中的算法，训练数据覆盖程度未知；工作流对未发表或此前未见算法、以及对已有源代码而非论文描述的表现尚未确立；没有与人工主导验证的对照，也未分离流程各组成部分各自的贡献；正确性结论仍取决于人工审阅的规格是否准确以及 Dafny 及其底层求解器的可靠性。