大语言模型使用TLA+建模真实系统的工程可行性分析

当我们要求大语言模型为真实系统编写 TLA + 规范时，会发生什么？表面上，模型可以生成语法正确的形式化描述、通过 TLC 模型检查器的运行时检查、甚至在简单的并发原语上表现出近乎完美的行为。然而，当评估深入到规范与实际代码的一致性时，差距急剧显现 —— 最新的前沿模型在一致性检查阶段平均仅获 46% 得分，在不变量验证阶段更是低至 41%。这一现象揭示了形式化验证领域的一个根本性挑战：编写「看起来像 TLA + 的代码」与真正「建模一个真实系统」之间存在难以逾越的鸿沟。

SysMoBench 基准测试的设计思路

理解这一问题的最佳切入点是 SysMoBench—— 一个专门用于评估大语言模型 TLA + 建模能力的自动化基准。SysMoBench 选取了十一个真实系统作为建模对象，涵盖并发同步与分布式协议两个领域，包括 ZooKeeper Fast Leader Election、Etcd 的 Raft 实现、RedisRaft、CURP 等复杂分布式系统。每个任务提供源代码、Trace 收集工具和不变量模板，要求模型生成的规范能够通过四阶段评估：语法检查阶段验证 TLA + 模块是否可被 SANY 解析器接受；运行时阶段检查 TLC 模型检查器能否正常执行该规范；一致性阶段通过 Trace 验证方法 —— 即对比真实系统执行产生的状态迁移序列与规范所描述的迁移是否匹配；不变量阶段则检查规范是否满足关键的安全性与活性属性。

这四个阶段的设计初衷在于区分两种截然不同的模型输出：一种是复述教科书式的标准协议描述，另一种是真正反映特定系统实现细节的忠实建模。前两阶段的通过率极高，因为网络上存在大量 TLA + 示例，模型能够轻松学习到标准的语法结构和惯用模式。但一致性阶段和不变量阶段才是真正的试金石，它们要求模型理解目标系统的具体实现逻辑：如何分解原子操作、如何组织状态数据结构、状态迁移在何种条件下触发。

两种系统性失败模式

当在 SysMoBench 上测试当前领先的大语言模型时，两种系统性的失败模式反复出现。第一种模式是规范进入了真实系统永远不会到达的状态。模型按照形式化方法教材中的标准模板编写规范，却未注意到目标系统实际使用的数据结构与模板假设不同。以 ZooKeeper Fast Leader Election 为例，ZooKeeper 代码中每个服务器的 recvset 是一个以发送者为键的 Map—— 当同一 peer 在新轮次发送新投票时，它会覆盖该 peer 的旧投票。然而，Claude Sonnet 生成的规范使用了集合并集操作recvVotes' = recvVotes ∪ {newVote}，同时保留旧投票和新投票。这种「累积所有投票作为证据」的模式常见于形式化方法教材，但与 ZooKeeper 的语义并不匹配。结果是，每当 peer 的投票在轮次之间发生变化时，规范的后状态同时包含旧投票和新投票，而真实系统只保留新投票。一旦下游的 quorum 检查依赖于投票计数，规范就会进入真实代码永远不会产生的状态。

第二种失败模式恰好相反 —— 规范无法到达真实系统必然进入的状态。模型将代码中的多个步骤合并为单个原子 guard，导致规范中的迁移在真实系统能够触发的条件下被禁用。仍以 ZooKeeper 为例，HandleNotification 动作携带了一个 guard m.electionEpoch <= logicalClock[s]，用于检查传入消息的 epoch 是否高于本地的 logicalClock。如果更高，该动作被禁用。但 ZooKeeper 的代码处理逻辑并非如此：当服务器收到更高 electionEpoch 的消息时，它首先将本地的 logicalClock 增加到与消息匹配的 epoch，然后再处理消息。这两个步骤在代码中按顺序发生。然而，模型将它们融合成单个 guard，从而抹去了代码在每个选举轮次都会进入的状态 ——local epoch 等于 1 而传入 epoch 等于 2 的瞬间。

这两种失败模式的共同根源在于：模型生成的是结构完整、类型正确的 TLA + 模块，但它们遵循的是教科书式的形式化模板，而非反映实际实现。模型知道 Raft 和 ZAB 作为协议是什么样的，但它不知道 Etcd 或 ZooKeeper 如何将特定动作分解为多个步骤。这是为什么仅靠语法和运行时评估远远不够的原因 —— 模型生成的规范都能通过 SANY 解析器的检查，因为它们在结构上是完整的。要区分「建模 Etcd」与「复述 Raft 论文」，评估必须到达一致性和不变量阶段，询问每个动作的迁移是否与系统在运行时实际产生的状态变更相匹配。

量化结果与能力边界

在十一个系统上测试当前领先的大语言模型（Claude、GPT、Gemini、DeepSeek、Kimi、Qwen 等）后，得分模式呈现出清晰的层次结构。语法阶段几乎所有模型都接近满分 —— 几乎每个前沿模型都能写出语法有效的 TLA + 规范。运行时阶段已经开始出现分化，得分范围从 30% 到 92% 不等。真正的差距出现在一致性和不变量阶段：不变量阶段最弱的模型仅有 16% 的得分，而 Gemini 3.1 达到了 81% 的最高分。这种模式在不同系统级别上保持一致：在 Asterinas Spin、Mutex、RwMutex 等简单系统上，几乎每个模型都能从第一阶段顺利通过到第四阶段且得分很高；但在 Etcd、RedisRaft、CURP、PGo raftkvs 等复杂分布式系统上，模型在第一阶段全部获得 100% 或接近 100% 的得分，但从第二阶段开始就出现崩溃 —— 有些模型甚至无法让 TLC 正常运行，而那些能够运行的模型在一致性和不变量阶段的得分也仅在 10% 到 50% 之间。即便是能力最强的 Claude Sonnet 4.6，在 RedisRaft 和 CURP 上的总体得分也仅有 25%。

这些数据揭示了一个关键洞察：编写一个能够编译的 TLA + 模块是可实现的目标，但让该模块与特定系统的实际行为保持对齐则困难得多。高语法得分很大程度上反映了训练数据中 TLA + 示例的丰富程度。一旦评估要求模型像真实代码那样分解动作并匹配状态与数据结构，之前的学习示例就不再有帮助。分别评估一致性和不变量粒度才能区分「在写 TLA+」与「在建模一个特定系统」。

从模型到智能体：Specula 的实践

面对这一挑战，研究团队探索了超越单纯语言模型输出的路径。他们发现，像 Claude Code 和 Codex 这样的前沿代码智能体已经具备更强的 TLA + 建模能力 —— 这些智能体能够自主读取目标代码库、决定建模范围、驱动完整的规范工作流。基于这一发现，研究团队开发了 Specula，一个专门用于 TLA + 形式化建模的智能体系统。Specula 在当前的 SysMoBench 任务上实现了一致性和不变量阶段的满分通过，这一结果出现在 SysMoBench 的公开排行榜上。

Specula 的核心突破在于将 TLA + 建模视为一个迭代式的问题解决过程，而非一次性生成。它首先分析目标代码的结构，识别关键的原子操作和数据结构；然后生成初始规范并通过 Trace 验证进行检验；当发现不一致时，智能体能够回溯分析失败原因，调整数据抽象粒度或动作分解方式，直到规范与真实系统的行为完全对齐。这种智能体架构代表了 AI 辅助形式化验证的一个重要方向 —— 从「生成规范」到「验证并修正规范」的闭环工作流。

工程实践中的现实挑战

将大语言模型或智能体应用于 TLA + 形式化建模时，仍有若干工程挑战需要谨慎处理。首先，窗口级评估严重依赖于 Trace 采样的覆盖率。过渡验证无法评估那些 Trace 未曾覆盖的代码路径。例如，在一次运行中 Asterinas RwMutex 的 AcquireUpReadLock 动作出现了零窗口 —— 并非因为规范失败，而是因为 upread () 代码路径在该 Trace 中根本没有被执行。系统性地扩展 Trace 覆盖范围仍是一个开放问题。

其次，状态抽象不可避免地丢失信息。将变量 log 表示为 (logLen, logLastTerm) 对，对于需要深入检查 log 内容的动作（如 HandleAppendEntries 检查特定中间条目的 term）是信息损失的。当前在过渡验证模块中通过手工方式缓解这一问题，但缺乏系统性策略。

第三是跨任务的可扩展性。添加新系统仍然需要手写的工具 harness、不变量模板和过渡验证模块。研究团队正在为这一流程搭建自动化框架，但完全自动化仍需要更多的工程投入。

对于希望在工程实践中应用这一技术的团队，建议采取以下策略：将 Trace 收集与规范开发同步推进，确保覆盖关键的代码路径；在一致性验证失败时，优先检查数据抽象层面的差异而非立即修改逻辑；将 AI 生成的规范视为起点而非终点，通过 TLC 的计数器示例进行迭代验证。对于复杂系统，考虑使用类似 Specula 的智能体架构来处理多轮迭代的建模 - 验证 - 修正循环。

资料来源：本文核心事实来自 SOSP 2025 会议论文及 Specula 团队发布的 SysMoBench 基准测试报告，相关代码与排行榜见 https://github.com/specula-org/SysMoBench 与 https://sysmobench.com。

ai-systems