LSP + LLM + 形式化验证器：Eiffel-tools 的可重试闭环

自然语言规格转代码是件容易的事。难的是，规格本身是怎么来的？

两条路的分歧

当前 LLM 用于软件工程的主流范式可以分成两派：

Spec-Driven 路线：人先把规格写清楚（自然语言或形式化），LLM 根据规格生成代码，用测试验证正确性。这条路假设规格先于实现，是正确性的根基。问题在于：规格在实践中往往是最后才写对的——代码和规格之间的迭代反馈，才是规格逐渐精确的过程。

验证器路线：不依赖人写规格的能力，而是把 LLM 嵌进一个「生成→验证→反馈→重试」的循环里，用形式化验证器作为最终的收敛标准。Eiffel-tools 走的是这条路，而且它用 LSP 作为这整套循环的中间协议层。

论文标题：Large Language Models and Language Server Protocol: a match made in context
作者： Alessandro Schena, Ilgiz Mustafin, Julia Kotovich（Constructor Institute）
发表：VERIFAI 2026
链接：arXiv:2609.03086

Eiffel 语言：一个天然适合形式化验证的环境

Eiffel 是少数把规格写进代码的语言之一。它的 Design by Contract 机制允许在方法上直接写前置条件（precondition）、后置条件（postcondition）和类不变量（invariant），这些不是注释，是语言一等的构造，可以在运行时检查，也可以在编译时用 AutoProof 做静态证明。

这意味着一个 Eiffel 项目天然同时拥有「可执行代码」和「形式化规格」——两者的一致性可以被数学证明，而不是靠测试覆盖。

但 Eiffel 是低资源语言：公开代码少，LLM 训练数据里几乎不存在。这意味着通用 LLM 对 Eiffel 的代码生成能力很弱。

Eiffel-tools 要解决的就是这个问题：不是让 LLM 凭直觉写 Eiffel，而是给它足够的上下文和验证反馈，让它在一个有证明保障的循环里逐渐逼近正确实现。

架构：LSP 作为三层之间的协议

Eiffel-tools 的架构可以分成四层：

┌──────────────────────────────────────────────┐
│  IDE / Editor（Client）                       │
│  ↕ LSP                                       │
├──────────────────────────────────────────────┤
│  Eiffel-tools（LSP Server）                   │
│  - 解析项目结构、类、特征、契约                │
│  - 构造 programmatic prompt                   │
│  - 管理 LLM ↔ 验证器的重试循环                 │
│  ↕                                            │
│  ┌────────────┐    ┌──────────────────────┐  │
│  │  LLM API   │    │  AutoProof Verifier  │  │
│  └────────────┘    └──────────────────────┘  │
└──────────────────────────────────────────────┘

LSP 层提供什么

LSP 标准化了语言服务器和编辑器之间的接口，包括代码补全、诊断、代码操作等。Eiffel-tools 利用 LSP 的「代码操作/命令」机制，把 LLM 生成代码的能力嵌进 IDE——

编辑器里触发一个命令（比如「修复这个特征的主体」），LSP 服务器收集：

  • 当前特征的契约（前置/后置条件）
  • 继承树和类层级
  • 相关特征的接口
  • 项目级类型信息

这些不是塞进自然语言 prompt 的模糊描述，而是程序化构造的精确上下文——LLM 知道「这里有一个 require 子句要求 x > 0」，而不是「确保输入有效」这样的模糊表述。

LLM 层

根据 programmatic prompt 生成 Eiffel 代码和规格。论文测试了三个模型：小通用模型、小编程模型、大编程模型（具体模型名在全文中）。

验证器层

AutoProof 是 Eiffel 的形式化验证器，基于 Boogie 和 SMT 求解器。它可以数学证明代码是否满足契约——不是测试覆盖，而是穷尽所有执行路径的证明。

当 LLM 生成的代码通过 AutoProof 证明，验证就完成了。如果没有通过，AutoProof 返回反例（counterexample），这个反例会作为 feedback 重新送入 LLM prompt。

重试层

这是 Eiffel-tools 最关键的设计：它不要求 LLM 一次生成正确的代码，而是允许一个重试循环：

  1. LLM 生成代码 → AutoProof 验证
  2. 验证失败 → 把错误信息 + counterexample 注入 prompt
  3. LLM 生成修正版本 → 重复

论文评估了这个循环的 effectiveness：2 个公开数据集 × 3 个模型，bug 修复率 76%–95%，取决于模型大小和 prompt 策略。而且重试次数和成功率之间存在明确的 tradeoff——更多的重试尝试带来更高的修复率。

为什么这条路线比 Spec-Driven 更硬核

Spec-Driven 的核心假设是：人能把规格写对。但实际工程中，规格的错误、遗漏、歧义往往在看到代码实现之后才暴露——这正是需求工程里「晚期需求涌现」现象的另一面。

Eiffel-tools 的思路是把规格从「先决条件」变成「验证副产品」：LLM 生成代码，验证器检查契约符合性，如果不符合，counterexample 会告诉你哪不符合。开发者不需要预先写出完整精确的规格，而是通过迭代逐渐让它收敛。

这和传统的 TDD 有一个关键区别：TDD 的测试是「人来写的不完整规格」，AutoProof 的证明是「数学上完备的正确性保证」。

对软件工程 Agent 架构的启示

1. LSP 是 Agent 上下文的天然接口

Eiffel-tools 最重要的贡献可能不是结果数字，而是证明了 LSP 可以作为 LLM 与静态分析工具之间的协议层。LSP 提供的项目级语义（类型、继承、特征签名、契约）比任何自然语言 prompt 都更精确，而且可以在编辑器里实时获取。

这对其他语言的 Agent 集成有直接参考价值：与其给 LLM 一个包含「项目概览」的静态 prompt，不如让 Agent 通过 LSP 动态获取上下文，在需要的时候精确查询。

2. 验证器负责证伪，LLM 负责猜想

这个分工在工程上比「让 LLM 自己保证正确」更可靠。Eiffel-tools 的设计本质上是把 LLM 看作一个高效的搜索 oracle：它生成候选解，验证器判断对错，反馈引导下一轮搜索。这和 AlphaZero 的 self-play 逻辑有相通之处。

3. 低资源语言反而更适合这条路

论文指出了一个反直觉但合理的结论：Eiffel 作为低资源语言，LLM 的直接生成能力很弱，但 Eiffel 的规格是可执行的、AutoProof 是现成的。这意味着上下文+验证反馈的价值在高不确定性环境下更高——模型不确定时，精确的验证反馈比模糊的直觉更有效。

4. 对幻觉问题的结构化解法

LLM 幻觉是 Agent 编程的主要障碍。Eiffel-tools 证明：在有形式化验证器的场景下，「幻觉」可以被自动发现并纠正，而不依赖人工 review。这比「prompt 优化」的路线更根本——不是减少幻觉的产生，而是让幻觉无法通过验证层。

局限性和开放问题

  • Eiffel 有现成的形式化规格体系（Design by Contract），这对其他语言不一定可迁移
  • AutoProof 只支持 model-based contracts，不是所有 Eiffel 特性都能验证
  • 重试循环的成本（延迟、token 消耗）没有在论文中详细分析
  • 评估只在 Eiffel 这个单一语言上做了，跨语言泛化需要进一步验证

小结

Eiffel-tools 的核心贡献不是「LLM 能修 Eiffel bug」，而是示范了一种可工程化的 LLM+验证器协作协议：LLM 负责生成，验证器负责证伪，LSP 负责提供精确上下文，三者通过一个自动重试循环串联起来。

这条路线比纯 Spec-Driven 更「硬核」，因为它不依赖人先把规格写对；它依赖的是「验证层能识别错误」——这是一个比「人写对规格」更可靠的假设。

当你的 Agent 还在靠 prompt 优化对抗幻觉时，这条论文指向了另一条路：把幻觉变成验证器的 input，让验证器把它过滤掉。