TLA+ Foundation Established to Drive Adoption of Proven Formal Methods for Robust Software.
SAN FRANCISCO, April 21, 2023 -- The Linux Foundation, the nonprofit organization enabling mass innovation through open source, today 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 Amazon Web Services (AWS), Oracle and Microsoft.
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.
“The establishment of the TLA+ Foundation demonstrates a commitment to advancing the use and development of the TLA+ language for the benefit of the entire software industry," said Jim Zemlin, executive director at the Linux Foundation. "As the world’s reliance on distributed systems grows, it’s important for developers to have TLA+’s capabilities to formally model and verify systems behave as they were intended."
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.
“AWS is committed to delivering high-quality services to our customers, which is why our Automated Reasoning team has relied on techniques like formal specification and model checking for years to solve difficult design problems in critical systems. TLA+ is a powerful tool in our toolbox that helps us to verify the correctness of our software systems under assumptions. By joining the TLA+ Foundation, we aim to support the advancement of TLA+ tooling and further improve the state of the art in distributed systems design,” said Byron Cook, Vice President and Distinguished Scientist at AWS.
“Across Microsoft, a growing number of engineering teams have been relying on TLA+ for specifying and validating the correctness of their algorithms and software systems. The engineering teams using TLA+ have reported tremendous value in precisely defining the systems and validating them earlier in the engineering lifecycle. The TLA+ tools have helped identify issues with their designs before writing a single line of code. By joining the TLA+ Foundation, we aim to foster a community of TLA+ practitioners who care deeply about designing correct distributed systems,” said Dharma Shukla, Technical Fellow at Microsoft.
“High scale distributed cloud services form the backbone of all hyperscaler cloud platforms, including Oracle Cloud Infrastructure (OCI). When we launched in 2016, OCI was the first cloud designed using formal methods from the start to deliver high quality cloud services. At OCI, we use TLA+ on more than 25 of our most critical services, including block storage and file storage services, to verify the correctness of complex design scenarios including distributed replication, failover and live re-sharding. We are excited to join TLA+ Foundation as a founding member with the goal of furthering the TLA+ toolkit and improving the quality of distributed cloud services in the years to come,” said Pradeep Vincent, SVP and OCI Chief Technical Architect, Oracle.
"The TLA+ Foundation is timely in so many ways. Thinking systemically and analytically about software development is more needed now than ever. The complexity of often-networks software systems is going up and we need tools like TLA+ to cope,” said Vint Cerf, Vice President and Chief Internet Evangelist at Google.
“Since its inception in 2020, Informal Systems has been using TLA+ to specify blockchain protocols such as Tendermint Consensus, the light client protocol, and the Inter-blockchain Communication Protocol (IBC). In combination with the Apalache model checker, these specifications reinforced the trust of the Cosmos community in these protocols. The flexibility of TLA+ also lets us bootstrap the security audits programme in a short timeframe. We applied Apalache for finding security issues in distributed applications powered by the Cosmos Technology,” said Igor Konnov, Principal Research Scientist at Informal Systems.
“Inria is committed to fostering research at the highest international level as well as to transferring the results of that research so that they have an impact on industry and society. Inria researchers have contributed to the evolution of the TLA+ language and to the design of verification tools for TLA+. The creation of the TLA+ Foundation helps ensure that the further development of the language and its tools will be a joint effort of the larger academic and industrial community interested in the design of trustworthy distributed systems,” said Stephan Merz, Senior Researcher at Inria and Head of the VeriDis project team.
“NVIDIA actively uses formal methods in the development of safety/security critical software and hardware, including TLA+, which we use to formalize our designs and requirements. We see the TLA+ Foundation filling an important gap by providing a professionally managed platform to share contributions, experiences, and best practices. It can become a driving force to further improve the TLA+ product: enhance the TLA+ language, make model checking more powerful, and make the tools easier to use. Independent and open collaboration within the foundation is needed to secure the future of TLA+ as an actively developed and popular ecosystem. The TLA+ foundation fulfills another important need; promoting the wider use of formal methods in industry to improve product quality; especially where safety and security are critical,” said Tom McReynolds, Senior Director DRIVE OS SW, NVIDIA.
The TLA+ Foundation invites technology companies to join and support its mission to promote the development of TLA+ in the software industry. By working together, the TLA+ Foundation can continue to enhance the capabilities of this important language and help ensure that the benefits of TLA+ are available to all.
For more information about the TLA+ Foundation, please visit https://foundation.tlapl.us
Join TLA+ Foundation members for the educational Webinar “Mastering Concurrent Algorithms with TLA+” on June 14th, at 8:00 am PT. Register here.
Media Contact
Noah Lehman