TLA+ is a high-level programming language designed to model complex, concurrent, and distributed systems. This language was created by Leslie Lamport and is supported by major tech companies such as Amazon Web Services, Microsoft, and Oracle. Recently, TLA+ (Temporal Logic of Actions), a programming language used for modeling programs and systems, particularly concurrent and distributed ones, has moved from Microsoft’s jurisdiction to the Linux Foundation. It is now getting its own, separate foundation to promote its adoption and development.

The newly-launched TLA+ Foundation is an independent non-profit organization that aims to fund research, provide education and training, develop tools, and create a community of practitioners dedicated to fostering the use and development of TLA+. The foundation’s inaugural members include Amazon Web Services, Microsoft, and Oracle.

According to the Linux Foundation, TLA+ has been instrumental in verifying complex software systems, reducing errors, and improving reliability. The language is designed to detect design flaws early in the development process, which can save resources and time. TLA+ is based on the idea that simple mathematics is the best way to describe things precisely, and its tools are useful for eliminating fundamental design errors that are difficult to find and expensive to correct in code.

Leslie Lamport, a distinguished scientist with Microsoft Research, invented the language. Among the companies that use TLA+ is Oracle, which has used it to model more than 25 services of Oracle Cloud Infrastructure. This includes block storage and file storage services, as well as verifying the correctness of complex design scenarios such as distributed replication, failover, and live re-sharding.