LLM 时代如何构建可靠的软件系统

Quint 的诞生，源于我们对提升软件可靠性的关注。这也是 Informal Systems 自创立以来的使命。我们希望构建一个人人都能信任自己所用软件的世界。

LLM 改变了我们编写代码的方式，但也带来了新的挫败感。相信大家都经历过：盯着一份由 AI 生成的巨型 diff，却完全不知道它到底对不对；AI 用一段看似可以运行、实则暗藏错误的代码骗过了我们；测试全部通过，却根本没有测到任何有意义的东西。LLM 的核心能力就是生成看起来正确的文本——而这恰恰让验证变得异常困难。

AI 过度自信，需要接受现实检验。

但令人看到希望的是：LLM 也让我们能够用少得多的时间投入来保障可靠性。不，这并不只是让 AI 生成 spec，也不是“把 AI 塞进 Quint”。真正的问题是：在软件开发的新世界里，Quint 应该扮演怎样的角色，同时继续实现它诞生时的那个目标。

接下来，我想讲讲我们如何用 Quint 为 LLM 设置护栏，让它在一个复杂代码库中完成一项重大的核心改动，并让我们对结果充满信心。

Quint 如何融入这个故事

LLM 面临的根本挑战是验证。LLM 擅长生成代码，但我们人类很难仅靠 code review 来验证代码的正确性。通常，我们会结合自然语言文档与代码进行判断，而事实证明，这两者都出奇地难以验证。

Quint 解决这个问题的方式，是处在英文描述与代码之间，成为一个理想的验证点。它比代码更加抽象，因此更容易推理；同时又不像英文那样无法执行，因此能够接受机械化验证。Quint 提供的 simulator、model checker 和 REPL，让你能够通过探索与属性检查逐步建立信心。

但实际代码又该如何验证？由于 Quint 是可执行的，我们可以通过 model-based testing，在 specification 与 implementation 之间建立确定性的联系：在 spec 和代码中运行相同的场景，然后验证两者的行为是否完全一致。这样一来，你在 spec 层面建立的信心就能传递到代码层面。

用例：在复杂系统中完成复杂变更

我们在 Malachite 上测试了这种方法。Malachite 是一个生产级 BFT 共识引擎，实现了 Tendermint 共识协议。这不是一个玩具示例——如果这种方法在这里行得通，那么面对更简单的变更和系统时自然也能奏效。Malachite 是一个复杂系统，在 Tendermint 之上实现了多项优化，仅共识核心就由四个不同的组件构成。

Malachite 被 Circle（USDC 背后的公司）收购，用于构建其新公链 Arc。Malachite 的许多协议设计从一开始就是使用 Quint 完成的。

这次变更是：切换到 Fast Tendermint。它是 Tendermint 的一种变体，需要 5F + 1 个节点才能容忍 F 个 Byzantine 节点，而经典方案只需要 3F + 1；作为交换，它有望通过减少一个通信步骤获得更好的性能。

按照传统方式估算，这项变更需要几个月。

我们挑战自己，要借助 Quint 和 AI 在一周内完成它。最终，我们做到了。

我们已经有了一份 Spec

我们的起点是一份现有的 Quint Tendermint spec，具体来说，是一份使用 Choreo framework（我们用于建模分布式系统的 framework）的 spec。我们拥有许多不同版本的 Tendermint spec，因为这是我们最喜欢建模的协议。

AI 能替你编写第一份 spec 吗？它当然可以提供帮助，而我们也在探索更多扩展这种帮助的方式。即使第一份 spec 必须由你手动编写——对于一个复杂协议来说，这通常需要几天——其在复杂系统中的 ROI 依然非常可观：这笔初始投入会在之后的每一次变更、重构或优化中持续产生回报。

把 LLM 当作翻译者，而非设计者

我想明确一点：我们并没有把协议设计交给 AI，也没有要求 AI 去设计最先进的 BFT 共识算法。

真正的工作由 Manu 完成，他是我们最优秀的协议设计者之一。他负责研究、编写英文协议说明、起草证明和论文。我们想验证他的协议是否正确，这正是 Quint 发挥作用的地方——只不过这一次，还有 AI 从旁协助。

因此，我们从两份材料开始：一份原始 Tendermint 的 Quint specification，以及一份新 Fast Tendermint 的英文说明。

工作流：通过四个步骤建立信心

输入：现有 Tendermint spec + Manu 的英文协议说明
过程：AI 根据新协议修改 Quint spec
输出：第一版 Fast Tendermint spec

每次变更后，我们都会运行 Quint 的基础验证工具：使用 quint parse 检查语法，使用 quint typecheck 验证类型、引用和函数签名。这个紧密的反馈循环可以在继续推进之前立即发现基础错误，并通过不断迭代，最终得到一份结构健全的 spec。

但结构健全并不等于行为正确。

这才是人类应该投入大部分时间的地方。省下来的代码编写时间，现在可以用于更深入的验证。

你可以通过交互方式查询 spec：“能否到达发生 X 的场景？”“这个属性是否成立？”AI 帮助你使用 Quint 的工具，而你则贡献领域知识。AI 可以提出一些场景建议，再由你引导它，逐步增强自己对结果的信心。

对于 Fast Tendermint，我们验证了以下内容：

重新广播机制：我们能否触发重新广播？能否接收重新广播并采取行动？

重新广播机制：我们能否触发重新广播？能否接收重新广播并采取行动？

替代决策传播机制：这个机制会在什么情况下取代正常流程被触发？我们找到了这些场景，并将它们记录下来。

替代决策传播机制：这个机制会在什么情况下取代正常流程被触发？我们找到了这些场景，并将它们记录下来。

Byzantine 容错假设：我们指定了一个包含过多 Byzantine 节点的版本。在这个 model 中，各节点应该有可能出现分歧。如果不能，就意味着我们在 model 中作出了不切实际的假设。

Byzantine 容错假设：我们指定了一个包含过多 Byzantine 节点的版本。在这个 model 中，各节点应该有可能出现分歧。如果不能，就意味着我们在 model 中作出了不切实际的假设。

目标是：测试所有流程是否均可到达，并系统性地探索状态空间。当我们确认覆盖范围足够充分后，就开始检查属性。这个过程重新建立了人与系统之间的连接——与 AI 生成代码后，你只能祈祷它没写错的那种疏离感截然相反。

结果是：我们仅用一个下午，就在 Manu 的英文 spec 中发现了两个小 bug。在这个阶段，它们很容易修复。

当验证全部通过——所有流程均可到达、属性成立、假设得到验证——我们就拥有了一份值得信任的 spec。它将成为后续代码生成的 source of truth。

现在，我们已经有了一份经过验证的 spec。接下来该生成真正的 implementation 了。

好消息是：当 AI 有一份精确的 spec 可供翻译时，它非常擅长生成代码。我们把旧 Quint spec、新 Quint spec，以及两者之间的 diff 一并交给 AI——输入的是 formal model，而不是含糊不清的自然语言。

Malachite 包含抽象 spec 中未体现的架构复杂性，例如各种优化、存储决策等，因此我们需要引导 AI 作出这些决定。这也是我们专业能力与职业价值的一部分。

我们验证了 spec，但真正关心的其实是代码。Model-based testing 让我们能够确信，代码遵循了 spec 中那些已经验证过的行为。

AI 会生成连接 spec 与 implementation 的“glue code”。这些 glue code 会获取第 2 步产生的场景——即 witnesses（用于证明状态可达性的属性）或 quint runs——然后在代码中重放：它读取一个场景，调用 implementation 中对应的入口，并断言结果与 spec 的预测一致。最终，它会生成一套可以在 CI 中持续运行的测试套件。

除了 model-based testing，我们还在研究 trace validation：从代码实际运行的环境中获取 traces，例如测试环境、testnet 和生产环境，然后验证这些 traces 是否符合 spec。这样就闭合了整个反馈循环：你验证的不再只是代码“能够”按照 spec 行事，还能确认它在实践中“确实”如此运行。

这次重构成功了。我们修改了 Malachite 的核心共识机制——按照传统方式，这项变更预计需要数月——而我们修改并验证 spec 只用了大约 2 天，代码生成与测试则用了约 1 周，其中包括完善和调试。这个流程仍有许多需要成熟的地方，但我们对最终结果非常满意。

一项关键收益：把 Spec 作为调试指南针

我们发现了一个很重要的好处：经过验证的 Quint spec 能防止你在调试时钻进那些根本不是问题的问题里。我们反复遇到以下模式：

AI（阅读测试日志）：“我知道哪里错了——执行 Y 时，我们应该广播 X！”

AI（阅读测试日志）：“我知道哪里错了——执行 Y 时，我们应该广播 X！”

AI（阅读 Quint spec）：“等等，spec 表明我们在执行 Y 时不会广播 X，这是有意为之的。”

AI（阅读 Quint spec）：“等等，spec 表明我们在执行 Y 时不会广播 X，这是有意为之的。”

结果：立即跳过这一假设，转而调查其他可能性。

结果：立即跳过这一假设，转而调查其他可能性。

如果使用的是英文 spec，你难免会产生怀疑：“会不会是我们忘记把它写进文档了？会不会 spec 本身并不完整？”于是，你会浪费时间调查这些错误线索。但对于一份经过验证、且已经被你深入探索过的 Quint spec，你知道它是正确的。如果在执行 Y 时广播 X 确实是必要行为，那么验证阶段就应该已经暴露这一点。既然 spec 明确指出不应这样做，我们就可以有把握地排除这项假设，继续调查其他方向。

把 spec 当作确定性参考并信任它，可以节省大量调试时间。它能阻止人类和 AI 怀疑错误的对象。

还记得之前提到的那些挫败感吗？面对巨型 diff，却完全不知道它们是否正确？一轮轮没有结构的 prompt 让人感到与结果失去连接？测试虽然通过，却什么都没测到？

这套工作流解决了这些问题。交互式 spec 验证重新建立了人与系统之间的连接——你不再只是祈祷 AI 没有出错，而是能够主动探索并逐步建立信心。当 AI 根据一份经过验证的 spec 生成代码时，你就有了一个可以用来核对的确定性参考。Spec 会成为你的调试指南针，避免你钻进那些根本不存在的问题。Model-based testing 则能确保测试真正验证了重要的内容。

在 LLM 辅助开发中，可执行 specification 是理想的验证点。它们处在英文与代码之间的最佳位置：足够抽象，便于人类推理；又足够精确，可以接受机械化验证。真正能够克服 AI 过度自信的，不是更多 AI，而是更好的验证工具。

真正值得注意的是：Quint 最初是为了帮助人类推理复杂系统而构建的。把 Quint 交给 AI，可以为 AI 设置护栏，使它能够处理更加复杂的问题，同时又不至于让结果变得无法验证。我们让 LLM 去做它最擅长的事情：在 Quint spec、文档与 implementation code 之间进行翻译。LLM 不会思考，它只会翻译。真正负责推理的是 Quint 的确定性工具。

我们的工作正在从编写代码转向验证 AI 生成的代码。定义“正确”究竟意味着什么，已经变得极其重要——而这恰恰就是可执行 spec 的作用。

这套工作流——修改 spec、交互式探索、受引导的代码生成，以及 model-based testing——能够扩展到真实世界的系统。我们已经在 Malachite 上证明了这一点。

想亲眼看看它如何运作吗？我们正在为有兴趣把这种方法应用到自身项目中的团队进行首批演示。如果你正在开发分布式系统，例如共识协议或互操作性协议、大规模数据库；或者正在开发其他复杂系统，例如交易应用（如 DEX/CEX）、密码学协议（ZKP、隐私保护应用）；又或者你正在处理任何其他可靠性至关重要的复杂核心逻辑，欢迎预约咨询。我们会向你展示 demo，也很乐意与你一起探索我们能如何提供帮助。

感谢阅读。我们正在构建可靠软件的未来——每次从一份可执行 spec 开始。