SPDDWL：用交互式定理证明器做 LLM 受验证软件项目生成

论文概览

论文标题：Trustworthy Software Project Generation: a Case Study with an Interactive Theorem Prover

作者：Jian Fang, Yingfei Xiong（北京大学 高可信软件技术教育部重点实验室）

链接：https://arxiv.org/abs/2605.26017

发布时间：2026 年 5 月 25 日

LLM 辅助编程已经不是什么新鲜事了——Cursor、Claude Code 等工具让"用自然语言写代码"成为日常。但一个根本问题始终存在：LLM 生成的代码可以编译通过、跑完测试，却仍然在语义上出错。对于关键的状态转换逻辑，这种"看起来对但实际错"的情况极为危险。

形式化验证理论上可以解决这个问题——要求生成的代码满足机器检查的数学规范。但现有的探索大多聚焦在 Dafny、Frama-C 这类自动验证工具上，直接生成项目级受验证代码仍然困难重重。这篇论文问了一个新颖的问题：能不能用交互式定理证明器（ITP）——比如 Rocq（前 Coq）、Lean、Isabelle——作为 LLM 代码生成的后端？ 答案是：可以，而且效果出人意料地好。

核心思路：把证明状态变成修复信号

论文提出的 SPDDWL 工作流，本质上是在 LLM 和最终可执行代码之间插入一层"形式化硬约束"——LLM 不仅要生成代码，还必须为代码生成机器可检查的证明。如果证明通不过，说明代码有语义错误，ITP 编译器会返回具体的证明状态（哪个子目标未闭合），LLM 据此精准修复。

这与 Dafny 式自动验证有本质区别。Dafny 依赖 SMT Solver 自动推理，验证失败时通常只返回一个"超时"或"未知"，LLM 不知道问题出在哪里，只能盲目尝试——论文的对比实验证实了这一点。

SPDDWL 三阶段工作流

工作流分为三个阶段：

阶段 1：需求分析 → Coding Plan

需求分析 Agent 将自然语言需求转化为一份结构化的 Coding Plan（编码计划）。这份计划回答了四个问题：用什么类型表示领域概念、哪些纯函数需要实现、哪些副作用操作留在 Host 层、每个函数必须满足什么逻辑性质。

关键设计是：分析器对任何未明确指定的选择（如整数宽度、符号/无符号语义）不猜测默认值，而是向用户提问澄清，直到计划中所有决策都确定。这避免了"LLM 按自己的想法填补歧义"这个常见的错误来源。

阶段 2：合成与验证 → 证明状态驱动的修复循环

Coding Agent 根据 Coding Plan 生成 Rocq 函数定义和类型声明，Proving Agent 生成对应的形式化规约（Lemma/Theorem）和 Tactic 证明脚本。两者输出一起送入 Rocq 编译器检查。

如果编译失败——无论是类型错误还是证明未闭合——SPDDWL 将错误信息和相关代码上下文返回给对应的 Agent。这里的巧妙之处在于：Rocq 暴露的显式证明状态（"当前目标是什么、已有什么假设"）恰好是 LLM 最擅长处理的输入格式——它像一个结构化的对话提示，告诉 LLM "这里还没证明完，请继续"。

修复循环设置了一个 k 次尝试的上限。如果所有尝试都失败，Agent 会反思——重新检查定理陈述、函数体和类型定义是否忠实反映了原始需求——然后从头生成新的证明脚本。如果仍然失败，则将失败目标呈现给用户请求人工介入。但即使在最坏情况下，用户也只需要处理一个孤立的目标，而非从头编写全部代码和证明。

阶段 3：组合与提取

所有指令处理器验证通过后，SPDDWL 将它们链接成一个统一的 step 函数（接收状态和解码后的指令，分发到对应处理器），然后证明组合定理——step 函数保持所有全局不变量（寄存器文件长度恒为 32、x0 始终读为零、非 CSR 指令不改 CSR 等）。

最后用 Crane 工具将验证通过的 Rocq 定义提取为 C++ 代码。验证的核心保证适用于这些提取后的代码——前提是提取工具忠实保留语义（这一假设与 CompCert、CertiCoq 等验证系统一致）。Host 层的 I/O 和运行时集成（仅 88 行 C++）作为"未验证部分"留给动态测试。

实验评估：RISC-V RV32I 全指令解释器

论文选择了一个既非 trivial 又非过大的任务：实现 RISC-V RV32I 无特权模式全部 47 条指令的 CPU 解释器。

实验配置：

• 模型：Claude Opus 4.7 High
• 后端：Rocq 9.0.1（主实验）/ Dafny 4.11.0（对比）
• 时限：30 分钟
• 硬件：Intel Ultra 265k（4×20核），48GB RAM，Ubuntu 22.04

核心结果：

代码量不大，但关键不在于规模——而在于 1,859 行中的每一行函数定义都经过了机器检查的证明。这 821 行函数定义覆盖了 RV32I 全部指令的计算逻辑：整数算术/逻辑、移位、加载/存储、条件分支、跳转、内存访问和环境调用。

RQ2：Rocq vs Dafny 的对比

这是整篇论文最有启发性的发现。在同样的任务和同样的 30 分钟预算下，Dafny 后端未能完成验证。LLM 生成了 2,070 行 Dafny 代码，但无法为所有函数生成完整的 pre/post-condition 并通过验证。

失败模式很典型：Dafny 的 SMT Solver 超时时，返回的信息几乎不包含"为什么未证明成功"——没有证明状态、没有剩余子目标，Agent 只能不断尝试不同的验证条件，每次触发新的超时，直到时间耗尽。

相比之下，Rocq 的 Tactic 失败时返回一个具体的证明状态——当前未闭合的子目标是什么、上下文中有什么假设——这让 Proving Agent 有了一个明确的修复目标。论文将此总结为一个值得注意的设计原则：当验证后端由 LLM Agent 操作时，反馈质量（而非验证能力本身）可能是决定性因素。

RQ3：动态验证

尽管形式化验证覆盖了核心逻辑，Host 层的 I/O 和集成代码（88 行）是未验证的。论文采用两种互补的动态方法来评估整个可执行程序：

1. LLM 生成的测试：265 个测试覆盖全部 47 条指令，全部通过
2. AFL++ Fuzzing：12 小时，执行 9,820 万个输入，完成 211 个完整 fuzzing 周期，零崩溃、零挂起

这两组数字的意义在于：它们验证了"提取的受验证核心"与"未验证的 Host 层"之间的边界在实际运行中不出问题——尽管形式化保证不覆盖 Host 层，但在大量随机输入的冲击下，这个边界保持稳定。

方法论细节：Proof-Guaranteed Correctness

论文实现中最值得学习的一个设计是"证明保证的正确性"机制。它不只是让 LLM 生成代码然后验证，而是要求 LLM 同时生成实现和证明，两者必须通过 ITP 编译器的联合检查。

这本质上是利用 Curry-Howard 同构：Rocq 中，程序性质和类型是一回事，证明和程序是一回事。如果 LLM 生成的代码有语义错误，它就无法为这个错误代码构造出类型正确的证明项——编译器会拒绝。论文精确地表述了这一思想：LLM 无法"幻觉"出一个被接受的证明，就像它无法"幻觉"出一个通过类型检查的程序一样——编译器要么找到闭合的推导，要么拒绝。

这个设计的精髓在于：它不是靠 prompt 工程或后处理过滤来抑制幻觉，而是让幻觉在结构上不可能通过验证。

启示与思考

读完这篇论文，我有几点想法：

第一，ITP 作为 LLM 的"编译器"这个角色被严重低估了。 过去我们习惯把 ITP 看作人机交互的证明工具（需要大量人工编写 Tactic），但在 LLM Agent 的场景下，ITP 的显式证明状态恰好是 LLM 最擅长消费的"结构化反馈"。这不是巧合——ITP 的证明状态天然就是一种"对话式交互"的形式，而 LLM 恰好擅长对话式推理。

第二，"反馈质量决定 Agent 效能"这个发现具有普遍意义。 不仅限于形式化验证。在更广泛的 Agent 架构设计中，工具返回的信息格式和粒度可能比工具本身的能力更重要。SPDDWL 实验中的对比（Rocq vs Dafny）为这个直觉提供了坚实的实证支撑。

第三，效应分离（Pure Core + Effectful Host）是一种务实的折中。 不是把所有逻辑都塞进形式化验证（像 seL4 做的那样），而是只验证"确定性计算"的部分。这降低了形式化负担，同时仍然保证了核心逻辑的正确性。这个思路与 Rust 的 unsafe 块边界设计异曲同工——把"已验证"和"未验证"的边界清晰地标出来。

第四，局限性需要诚实面对。 论文的规约由 LLM 自动生成，这意味着规约本身可能不完备——如果有语义要求没有被写入规约，再严谨的证明也无法捕获。此外，提取工具（Crane）的正确性是被假设而非被证明的。论文对这两点都有讨论，但在实际安全关键场景中，这些差距需要更系统的方法来弥合。

第五，SPDDWL 对 Agent 形式化验证研究者的启示。 如果你在构建 Agent 安全框架（如 AgentMoss 这类基于形式化方法的工作），这篇论文提供了一个强有力的经验证据：ITP 后端的显式证明状态是比 SMT 超时更有效的修复信号。在选择验证后端时，反馈质量应该成为一个一级设计考量。

总之，这是第一篇系统性地探索"ITP 作为 LLM 软件生成后端"的实证研究。它的核心贡献不是算法创新，而是通过一个具体的非平凡案例证明了这条技术路线的可行性，并揭示了反馈质量在 Agent-driven 验证中的关键作用。

参考文献

1. 论文原文：https://arxiv.org/abs/2605.26017
2. Rocq Prover：https://rocq-prover.org/
3. Dafny：https://github.com/dafny-lang/dafny
4. Crane (Rocq to C++ extraction)：https://github.com/bloomberg/crane
5. RISC-V Unprivileged ISA：https://docs.riscv.org/reference/isa/unpriv/rv64.html