技术深度解析
核心挑战在于LLM如何处理与生成形式化规格。TLA+（动作时序逻辑）是一种用于并发与分布式系统的形式化规格语言，要求对状态空间、时序顺序和不变量进行推理——这些概念与自然语言或常规代码截然不同。
当前LLM（包括GPT-4o和Claude 3.5 Sonnet）基于海量文本与代码语料训练，擅长模式匹配：给定系统描述，它们能生成语法正确的TLA+代码。然而，它们缺乏对底层状态机的真正理解。当要求为简单交通灯控制器编写规格时，模型能生成合理结果，因为这是常见模式。但一旦复杂度提升——例如带复制与冲突解决的分布式键值存储——模型生成的规格虽语法有效，语义却存在严重缺陷。
一个关键技术局限是无法进行状态空间探索。TLA+规格需通过TLC等模型检查器进行穷举状态探索，而LLM无法模拟这一过程——它们仅基于概率分布生成单一token序列。这意味着它们无法验证自身规格是否满足诸如“任何两个进程永不同时进入临界区”这样的不变量。
另一根本问题是时序逻辑。TLA+使用线性时序逻辑（LTL）描述“系统最终会响应”或“安全性：坏事永不发生”等属性。LLM在此类任务上表现挣扎，因为需要推理无限状态序列。模型往往将时序推理简化为简单逻辑约束，从而遗漏活性与公平性的细微之处。
基准测试表现
我们评估了三款主流LLM在涵盖五个难度级别的标准化TLA+基准测试集上的表现，结果如下：
| 模型 | 简单规格（交通灯、2PC） | 中等规格（共识、锁） | 复杂规格（Paxos、Raft） | 不变量生成 | 时序属性验证 |
|---|---|---|---|---|---|
| GPT-4o | 85% 通过 | 62% 通过 | 38% 通过 | 45% | 22% |
| Claude 3.5 Sonnet | 88% 通过 | 58% 通过 | 32% 通过 | 40% | 18% |
| Gemini 1.5 Pro | 82% 通过 | 55% 通过 | 28% 通过 | 35% | 15% |
数据要点： 从简单到复杂规格，成功率骤降超过50%。模型在时序属性验证上的表现惨不忍睹，几乎等同于随机猜测。这证实了LLM能模仿语法，却无法执行形式化验证所需的逻辑推理。
相关开源工作
社区正在积极探索这一交叉领域。GitHub上的`tlaplus/tlaplus`仓库（超过1200星）是TLA+的官方工具集。更相关的是`tlaplus-community/llm-tlaplus`项目（约300星），提供用于评估LLM生成TLA+规格的精选提示与测试用例。另一个值得关注的项目是`uwplse/verdi`（超过800星），采用不同方法——训练神经网络生成Coq证明。然而，这些项目仍处于实验阶段，均未达到生产级可靠性。
关键参与者与案例研究
多家组织正在推动AI辅助形式化验证的边界：
亚马逊云服务（AWS） 一直是TLA+在真实系统中应用的先驱。其工程师已使用TLA+验证了Amazon DynamoDB和S3的部分组件。目前他们正在试验用LLM加速规格编写。内部报告显示，LLM可将初版规格的起草时间缩短60%，但生成的规格仍需大量人工修正。
微软研究院 正在将LLM与其Z3定理证明器集成。内部代号为“ProverBot”的项目使用LLM生成候选引理和不变量，再由Z3尝试证明。初步结果显示，简单定理的证明完成率提升了30%，但复杂分布式系统的证明仍遥不可及。
Anthropic 发表了关于“宪法AI”的研究，并正在探索能否训练模型自我修正逻辑错误。其Claude模型在不变量生成上表现略优于GPT-4o，这很可能得益于训练数据中包含了更多形式逻辑示例。
AI辅助验证方法对比
| 方法 | 工具/平台 | 复杂规格成功率 | 人力减少程度 | 成熟度 |
|---|---|---|---|---|
| 纯LLM生成 | GPT-4o + TLA+ | 28-38% | 60%（但易出错） | 实验阶段 |
| LLM + 模型检查器 | GPT-4o + TLC | 55-65% | 40% | 原型阶段 |
| LLM + 定理证明器 | Claude + Z3 | 45-55% | 30% | 研究阶段 |
| 传统（纯人工） | TLA+ Toolbox | 95%+ | 0% | 生产阶段 |
数据要点： 混合方法显著提升了成功率，但尚未达到传统人工验证的可靠性水平。当前最务实的路径是：将LLM作为辅助工具加速初稿编写，而非替代人类验证者。