TLA⁺ 开发的现状

发布于 2025 年 5 月 15 日 | Andrew Helwer

（一张加拿大鹅站在加拿大安大略省尼亚加拉瀑布的黄色蒲公英田野中的照片）

TLA⁺ 开发的现状

发布于 2025 年 5 月 15 日 | Andrew Helwer

2025 TLA⁺ 社区活动 上周 5 月 4 日在加拿大安大略省汉密尔顿的 McMaster 大学举行。 它是 ETAPS 2025 的一个卫星活动，我也参加了 ETAPS 2025，并计划在不久的将来撰写相关内容。 我做了一个有点推销性质的演讲，标题为 现在编写 TLA⁺ 工具比以往任何时候都更容易！，我将在此将其转化为对 TLA⁺ 开发现状的总体介绍。 会议的演讲都录制了下来，因此如果您想要以视频形式观看这篇博文，可以在下面观看：

大纲

本文的论点是，我们对 TLA⁺ 的几乎所有梦想和愿望都源于让开发 TLA⁺ 语言工具变得容易。 我们将其分解为三个部分：

  1. 现有 TLA⁺ 语言工具的概述
  2. 克服遗留代码的挑战
  3. 近期和中期未来的一些 TLA⁺ 开发想法

我对 TLA⁺ 的未来非常乐观，尽管存在挑战。 我们现在有了 TLA⁺ Foundation，在过去六个月里，它非常慷慨地支付给我舒适的生活工资来从事工具的开发工作。 我将谈谈我所完成的一些事情。 能够获得报酬来开发 FOSS 是一种幸福的存在； 如果您也觉得这很吸引人，TLA⁺ Foundation 正在 寻找更多贡献者！

现有工具

这是对现有 TLA⁺ 语言工具的总结，以激发您对可以贡献或构建的工具的想象力。

解析器

解析器当然是任何语言工具的基础，因为您的工具需要知道一些源代码实际上说了什么。 我们拥有一支不错的稳定队伍：

以上是三大解析器。 还有一些其他的解析器，处于不同的完成阶段：一个在 Python 中，Haskell，Haskell (再次)，和 Rust（我自己也写到一半，然后迷失在 Rust 类型系统的迷雾中并精疲力竭）。

解释器

沿着堆栈向上移动。 长期以来，我们只有一个解释器，现在我们有两个了！

模型检查器

再次沿着堆栈向上移动。 我们现在有 三个 模型检查器了！

其他

这是一系列其他值得注意的 TLA⁺ 语言工具：

总结一下

我认为 TLA⁺ 工具生态系统的当前状态 非常强大。 一旦我把所有这些都写出来，这一部分就很长了。 人们不仅想使用 TLA⁺，他们还想让它变得更好！ 这是社区中一种非常好的能量。 很多人不喜欢被束缚在 JVM 上，但替代方案正在慢慢形成。

克服遗留代码的挑战

许多工作的软件工程师都读过（或至少听说过）这本书： 它对遗留代码有一个简洁而客观的定义，我很喜欢：遗留代码是没有测试的代码。 但是，随着我职业生涯的成长，我得出了一个更模糊的定义：遗留代码是不存在于鲜活知识中的代码。 代码库甚至特定模块并不完全存在于从事它的开发人员的脑海中。 我们可能都从头开始编写过软件，并且知道进行大规模更改是多么容易，因为您知道每个部分是如何工作的。 如果你把同样的任务交给一个代码库新手，你可以合理地预期花费的时间会增加 10-100 倍才能达到同样的变化，并且代码库的最终状态将远不如原来的连贯。

我们在 TLA⁺ 项目中缺乏大量的鲜活知识，我将在下一节中进一步阐述。 本节的论点很简单：如果 TLA⁺ 要 蓬勃发展，我们必须克服这一挑战。 TLA⁺ 将依靠惯性缓慢前进一段时间，但如果我们不征服摆在我们面前的挑战，最终会发现自己变得无关紧要。

关于鲜活知识的最后一点说明：它与测试相互关联。 一旦鲜活知识丢失，就必须从头开始重建，只有当你可以为代码库编写测试时，才有可能做到这一点。 戳它并刺激它，看看它是如何流动和相互联系的。 大多数 高效处理遗留代码 都涉及如何在缺乏测试的代码库中安全地进行更改，而编写测试 需要 更改代码库以使其可测试。

TLA⁺ 面临的挑战

首先，快速回顾一下历史：Leslie Lamport 在 1990 年 4 月发表了论文 A Temporal Logic of Actions。 Jean-Charles Gregoir 在 1990 年代后期编写了最初的 SANY TLA⁺ 解析器。 TLC 模型检查器是在 25 年前编写的，在 1999 年的论文 Model Checking TLA⁺ Specifications 中由 Yuan Yu 和 Panagiotis Manolios 宣布，该论文描述了为 TLA⁺ 编写解释器和安全性检查器。 到 2002 年，活性检查器 已被开发出来。 这些工具随后在 2010 年左右进行了大量修改，以发布 TLA⁺ 2，其中添加了证明语言。 大约在这个时候，Inria 和 Microsoft Research 合作编写了 TLAPM，以便可以正式检查证明语言。 Inria 的资金在 2010 年代后期到期，TLAPM 的开发速度急剧下降。 Apalache 符号模型检查器的开发始于 2010 年代后期，并在 Informal Systems 在 2020 年代初将其引入内部时加速，但自从 Informal Systems 在 2024 年底分拆 Apalache 以来，开发速度也同样急剧下降。 TLA⁺ Foundation 的成立是为了支持 TLA⁺，因为它是在 Leslie Lamport 于 2024 年底退休之前从 Microsoft Research 分拆出来的。

我们将重点关注维护 SANY 和 TLC 的挑战。 与 SANY 和 TLC 相比，TLAPM 和 Apalache 对非学术软件工程师来说更难以接近，我将有兴趣观看关于如何加快其开发速度并使其可持续的演讲。

因此，我们有一个已有四分之一个世纪历史的 Java 代码库，由于大量的全局静态状态，很难进行单元测试，所有最初的作者早已离开该项目，并且三个常规的核心贡献者缺乏对其许多部分的了解。 我们每个人都专注于不同的领域：我倾向于研究解析器，Markus Kuppe 倾向于研究模型检查器，而 Calvin Loncaric 倾向于研究解释器，并且也是我们常驻的真正 Java 专家。 我们有很多想做的事情，但受到未知的限制。 这听起来有些可怕，那么我为什么乐观呢？

梦想和我们的祝福

让我们从一个梦想开始：一个我们大胆且不害怕对核心 TLA⁺ 工具进行重大更改的世界。 我们如何到达那里？

值得庆幸的是，我们从一个强大的地位开始。 语言工具是软件工程中一个令人欣慰的领域。 它是少数几个程序需求相对完整且明确的地方之一。 实际上可以 完成 解析器！ 通常，启动一个软件项目有点像给自己施加诅咒，你必须不断地提供你的劳动，否则它将从相关性中消失，而你所有的工作都将是徒劳的。 这里并非如此。 当然，传统的语言工具的需求随着时间的推移确实变得更强。 现在，解析器必须在语言服务器上下文中很有用，这需要比以前的标准更好的错误恢复能力。 但这些都来自开发文化中相对缓慢的变化，并且每十年左右才会出现一次。

具体策略

不要再浪费时间了。 以下是我认为将我们从梦想变为现实的三种策略：

  1. 测试 - 当然！ TLA⁺ Foundation 一直在资助我投入 大量 精力来开发 TLA⁺ 解析器的 标准化、独立于实现的测试套件，然后将它们应用于现有的解析器。 我们现在有一个不错的源代码输入/预期 AST 输出语法套件，应用于三个主要的解析器（有利于一致性！），以及一个具有大量关于级别和引用的语言内断言的语义级别测试套件（感谢 lobste.rs users 提供了一些关于其设计的绝佳建议），以及 - 我最喜欢的 - 一组 150 个 TLA⁺ 解析输入，每个输入都应该在任何一致的解析器中触发特定的标准化错误代码。 总而言之，我认为这些使得每个 TLA⁺ 解析器都可以进行开发！ 我们不再受限于通过 git-bisecting 和比较难以理解的代码来分析错误； 只需编写一个测试并在调试器中跟踪它即可！
  2. 开发人员入门 - 我们必须超越文档。 将代码库视为一个固定的工件，供任何新的贡献者研究和学习，然后为其制定教学大纲。 TLA⁺ Foundation 一直在以各种方式资助我这样做，例如编写 开发 和 贡献 指南，在 每月开发更新 中突出显示好的第一个问题，以及 - 最重要的是 - 编写一个关于 如何编写你 自己的 最小 TLA⁺ 模型检查器 的长篇教程！ 最后一个非常有趣，并且基于 Robert Nystrom 出色的免费在线教科书 Crafting Interpreters。 看看吧！
  3. 资助金和津贴 - FOSS 开发的基本矛盾在于，每个重要的 FOSS 项目都需要长时间的 全职 投入，但人们需要吃饭，而且很难通过免费赠送东西来赚钱。 当我刚开始接触这个游戏时，我以为 Linux 是人们在晚上和周末开发的。 对某些人来说是这样，但绝大多数代码都是由全职从事 Linux 工作的人贡献的！ 关于如何管理 FOSS 的基本矛盾，已经花费了大量的笔墨。 拥有公司赞助的基金会是一种方法，而这正是我们所拥有的。 TLA⁺ Foundation 可以资助人们从事工具的开发工作，而且他们正在这样做。 有兴趣吗？ 加入我们！

总结一下

因此，我们从一个强大的地位开始，并且拥有克服剩余挑战的具体策略。 我们还应该认识到，我们的斗争是共同的。 TLA⁺ 社区中的人们偶尔会说“TLA⁺ 不是一种编程语言”，但我们面临着与所有其他编程语言的开发人员相同的挑战！ 即使是 TLA⁺ 的奇异部分也“只是”算法。 我的意思是，与开发未知的代码库的挑战相比，学习算法相对容易、有趣且可控。 无论活性检查算法多么复杂，它“只是”一个关于图的算法，普通开发人员只需几天的时间学习即可，前提是有合适的教程。 而编写该教程并使其有趣是我们的工作。

接下来是什么？

我在演讲结束时提出了一些我对近期 TLA⁺ 工具开发的想法。 其中之一受到上个月参加 Antithesis BugBash 的启发，是 TLA⁺ 工具的生成式测试！ 将我关在办公室里来编写数百个测试用例当然很好，但是如果这个过程可以自动化呢？ 与开发大型静态测试语料库相比，开发它肯定会更有趣。 实际上，两者都拥有是很好的：静态测试用例用于确定核心语言功能，而生成式测试用于探索各个角落。

我还初步提出了简化 TLA⁺ 语法的建议。 我有点古怪，喜欢 TLA⁺ 语法（尤其是在其 Unicode 形式中），但其他人确实为此苦苦挣扎，正如 Hillel Wayne 可以从他在网上和线下教授 TLA⁺ 的工作中证明的那样。 我不是反对发展语法的纯粹主义者。 我认为我有一个 非常不错的 RFC，用于组合和消除集合过滤器和集合映射语法的歧义。 更大的变化将不得不进行辩论。 这是设计和共识工作； 相比之下，实际的代码更改可能不会很大。

我还想改进 SANY API 和消费体验，以便人们可以轻松地构建自己的工具，而不是请求将功能上游。 一个新的 API 已经进行了原型设计，并且所有 SANY 单元测试目前都在练习它。 Markus 还努力从滚动发布中自动 发布一个 Java 包。 最后，我们需要编写一系列关于如何使用和开发该软件包的指南。 实际上，TLA⁺ 领域中存在相当多的项目和功能，但尚未为其编写和传播文档。 我认为我可以花整整一年的时间只编写教程和文档。 我越来越相信这实际上是对时间的有效利用，甚至可能是我使用 TLA⁺ 的最佳方式。

每分钟 10 亿个状态倡议

我想用一个爆炸性的结尾来结束这次演讲，所以这就是：我认为我们可以通过编写 字节码解释器 将 TLC 模型检查器的吞吐量提高到每分钟 10 亿个状态（加速 1000 倍）。 目前，TLC 的时钟速度约为每分钟 100 万个状态。 Calvin 已经使用将 TLA⁺ 规范转译为 C++，然后将它们编译并作为小的广度优先搜索程序运行进行了一些 非常 初步的原型设计，并且看到了一些令人震惊的数字。 TLC 解释器是一个用 Java 编写的树状遍历解释器。 无论它如何优化，其格式的能力都有限。 这将是一个大胆而重要的项目，但我认为值得探索。

结论

感谢阅读！ 我希望这能够激励和启发您考虑开发自己的 TLA⁺ 工具或为现有工具做出贡献，同时对当前的状态进行很好的概述。

链接和讨论

Murat Demirbas 撰写了 一篇博文，介绍了他在 TLA⁺ 社区活动中的演讲，关于使用 TLA⁺ 来指定 MongoDB 中的跨分片事务。 他还写了一篇文章 总结了活动中的其他演讲。

A. Jesse Jiryu Davis 撰写了 一篇博文，介绍了他在 TLA⁺ 社区活动中的演讲，关于向 TLA⁺ 添加统计和性能建模功能的可能性。 他还发布了 他的笔记，介绍了活动中的其他演讲。

在这里讨论这篇文章：

tlaplus formal-methods