2023 年 4 月 21 日，非营利性组织Linux基金会于宣布成立 TLA+ 基金会，其中创始成员包括亚马逊、甲骨文和微软。与此之前，该组织通过开源实现大规模创新，现成立 TLA+ 基金会以促进 TLA+ 编程语言的采用及社区的发展。

TLA+ 是几十年前由计算机科学的开拓者 Leslie Lamport（现为微软搜索杰出科学家） 发明的，一种用于对程序和系统进行建模的高级语言，尤其是并发、分布式程序和系统。TLA+ 已被许多公司成功用于验证复杂的软件系统，减少错误并提高可靠性，有助于在开发过程的早期检测设计缺陷，从而节省时间和资源。TLA+ 及其工具可用于消除基本的设计错误，这些错误很难在代码中发现，并且纠正起来成本极高。经过 Lamport 多年的管理和微软的支持，TLA+ 在 Linux 基金会有了新的统一组织。

(资料图)

TLA+ 基金会将促进采用、提供教育和培训资源、资助研究、开发工具并建立 TLA+ 从业者社区。 TLA+基金会作为语言委员会将确保TLA+语言不断完善和演进，将就语言增强做出决策，解决用户反馈和需求，保持高安全性和可靠性标准，并引导语言的发展以更好地服务于其用户群。

作为初始成员加入 TLA+ 基金会的公司高层，针对自身公司业务与TLA+语言工具使用的重叠也有着不同的看法。

Linux 基金会执行董事 Jim Zemlin 表示：“随着世界对分布式系统的依赖程度不断提高，对于开发人员来说，拥有 TLA+ 的功能来正式建模和验证系统的行为是否符合预期非常重要。TLA+ 基金会的成立表明了我们致力于推进 TLA+ 语言的使用和开发，以造福整个软件行业”。

微软技术研究员Dharma Shukla 说：“在整个微软中，越来越多的工程团队一直依赖 TLA+ 来指定和验证其算法和软件系统的正确性，TLA+ 工具有助于在编写一行代码之前识别他们的设计问题，TLA+ 是 AWS 工具箱中的一个强大工具，可以验证软件系统在假设条件下的正确性。通过加入 TLA+ 基金会，旨在支持 TLA+ 工具的进步，并进一步提高分布式系统设计的最新水平。”。

Oracle 高级副总裁兼 Pradeep Vincent 说道：“大规模分布式云服务构成了所有超大规模云平台的支柱，包括 Oracle 云基础设施 (OCI)。在 OCI，我们在超过 25 个最关键的服务上使用 TLA+，包括块存储和文件存储服务，以验证复杂设计场景的正确性。很高兴作为创始成员加入 TLA+ 基金会，目标是在未来几年进一步发展 TLA+ 工具包并提高分布式云服务的质量”。

“TLA+ 基金会在很多方面都很及时，现在更需要系统地和分析地思考软件开发。网络软件系统的复杂性正在上升，我们需要像 TLA+ 这样的工具来应对”， 谷歌副总裁Vint Cerf 说道。

Informal Systems （可持续的技术网络组织）首席研究科学家Igor Konnov 说：“自 2020 年成立以来，Informal Systems 一直在使用 TLA+ 来指定区块链协议，例如 Tendermint 共识、轻客户端协议和区块链间通信协议 (IBC)。TLA+ 的灵活性还让我们能够在短时间内启动安全审计程序，提供支持的分布式应用程序中的安全问题”。

“ Inria 研究人员为 TLA+ 语言的发展和 TLA+ 验证工具的设计做出了贡献。TLA+ 基金会的创建有助于确保该语言及其工具的进一步开发，也推动对分布式系统感兴趣的学术界和工业界共同努力”， Inria（法国国立计算机及自动化研究院）高级研究员兼负责人 Stephan Merz 说道。

NVIDIA （驱动操作系统软件）高级总监 Tom McReynolds 表示：“NVIDIA 在安全关键软件中用 TLA+ 来形式化设计和要求，恰巧 TLA+ 基金会通过提供一个专业管理的平台来分享贡献、经验和最佳实践，填补了一个重要的空白。它可以成为进一步改进 TLA+ 产品的动力：增强 TLA+ 语言，使模型检查更强大，并使工具更易于使用”。

TLA+ 基金会的成立推动内部可以进行独立和开放的协作，以确保 TLA+ 作为一个积极开发的生态系统，还邀请各科技公司加入并支持其推动TLA+在软件行业发展的使命。通过合作，TLA+ 基金会可以继续增强重要语言的功能，并帮助确保所有人都能享受到 TLA+ 便捷与高效。

如果有开发者想了解 TLA+ 基金会的更多信息，可以访问 https://foundation.tlapl.us