Linux基金会宣布成立专门支持和发展TLA+（Temporal Logic of Actions）语言的基金会，主要创始会员为微软、甲骨文和AWS。TLA+是一种形式化的规范语言，可用于描述和检验分布式系统的行为、算法和协议。

TLA+语言最初是由Leslie Lamport在1990年代发明，其目的是要发展一个工具，协助工程师设计、理解和验证大型软件系统，特别是对那些具有高可性要求的系统。该语言的核心概念，是形式化数学公理，通过使用数学表示法描述系统的状态行为，让开发人员能够捕捉系统的重要属性，并且检验其是否满足特定需求，简单来说，TLA+语言让开发人员用简单的数学来描述系统。

支持时间逻辑（Temporal Logic）是TLA+的重要特性，允许开发人员能够表示和分析，系统在一段时间内变化的逻辑，利用这项特性，开发人员便能够更简单地发现，分布式系统中的竞争条件和死锁等常见问题。由于部分系统中的基本错误，很难从程序代码中发现，而且修正起来成本高昂，因此TLA+语言的价值，便是让开发者更简单地消除这些基本但是关键的错误。

TLA+语言发命者Leslie Lamport，目前是微软研究院的杰出科学家，在Leslie Lamport发明TLA+语言之后，受微软的支持和管理，现在微软决定将该项目贡献出来，在Linux基金会旗下成立TLA+语言基金会，以促进该语言推广、研究资助和工具开发等工作。