C’est le 21 avril que la Fondation Linux a créé une fondation spécifiquement dédiée au langage TLA+, dont la maintenance était jusque-là assurée par Microsoft. L’association indépendante à but non lucratif vise à favoriser l'adoption et le développement du langage de programmation TLA+ (Temporal Logic of Actions). Ce langage permet de modéliser des programmes et des systèmes, en particulier concurrents et distribués. La Fondation TLA+ assurera l'éducation et la formation, financera la recherche, développera des outils et créera une communauté de praticiens. Les premiers membres de la Fondation TLA+ sont Oracle, Microsoft et Amazon Web Services (AWS).
Selon la Fondation Linux, le langage TLA+ a été utilisé pour vérifier des systèmes logiciels complexes, réduire les erreurs et améliorer la fiabilité. Ce langage est censé détecter les défauts de conception dès le début du processus de développement afin d'économiser des ressources et du temps. Le langage TLA+ repose sur l'idée que la meilleure façon de décrire les choses avec précision est d'utiliser des mathématiques simples. Selon la Fondation Linux, TLA+ et ses outils sont utiles pour supprimer les erreurs de conception fondamentales, difficiles à trouver dans le code et coûteuses à corriger.
Le langage a été inventé par l'informaticien Leslie Lamport, aujourd'hui chercheur émérite chez Microsoft Research. Parmi les utilisateurs de TLA+ figure Oracle, qui a utilisé le langage pour modéliser plus de 25 services de l'Oracle Cloud Infrastructure, y compris les services de stockage de blocs et de fichiers, et pour vérifier l'exactitude de scénarios de conception complexes, notamment la réplication distribuée, le basculement et le re-sharding en direct.