The Linux Foundation has announced the launch of the TLA+ Foundation to promote the adoption and development of the TLA+ programming language and its community of TLA+ practitioners. Inaugural members include AWS, Oracle and Microsoft.

The TLA+ Foundation will promote adoption, provide education and training resources, fund research, develop tools, and build a community of TLA+ practitioners. The TLA+ Foundation’s role as the language committee will ensure the continuous improvement and evolution of the TLA+ language. The TLA+ Foundation will make decisions on language enhancements, address user feedback and needs, maintain high safety and reliability standards, and guide the language’s evolution to better serve its user base.

TLA+ is a high-level language for modeling programs and systems, especially concurrent and distributed ones. TLA+ has been successfully used by companies to verify complex software systems, reducing errors and improving reliability. The language helps detect design flaws early in the development process, saving time and resources.

TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code. The language is based on the idea that the best way to describe things precisely is with simple mathematics.

The language was invented decades ago by the pioneering computer scientist Leslie Lamport, now a distinguished scientist with Microsoft Research. After years of Lamport’s stewardship and Microsoft’s support, TLA+ has found a new home at the Linux Foundation.