cloudparts

TLA+ Foundation

The Linux Foundation’s fund behind TLA+, Leslie Lamport’s specification language: member dues pay for grants and tooling, while a Specification Language Committee decides what TLA+ is.

1 projects in this catalogPart of the Linux FoundationWebsite

What it is

The TLA+ Foundation is part of the non-profit Linux Foundation. Its charter took effect on January 10, 2023, and the LF announced it on April 21, 2023 with three inaugural members, Amazon Web Services, Microsoft and Oracle; Google, NVIDIA, Inria and Informal Systems sent supporting quotes. Formally it is a “directed fund”, set up to “raise, budget and spend funds in support of various open source, open data and/or open standards projects relating to TLA+”. Members must also be corporate members of the LF. Premier membership costs $100,000 a year and carries a seat on the Governing Board; General membership costs $5,000 to $20,000 depending on headcount, and General members elect one board seat per five members, up to three. In October 2026 the foundation listed three members: AWS, Oracle and NVIDIA, whose logo was added on July 21, 2026. Microsoft’s logo left the list in the spring of 2025, the year Lamport retired from Microsoft.

The fund holds the money; the code sits in separate legal entities. TLA+ itself is “TLA+ Project a Series of LF Projects, LLC”, under a technical charter adopted on January 5, 2023 that makes a Specification Language Committee (SLC) responsible for all technical oversight and puts outbound code under the MIT licence. Its first members were Stephan Merz (chair), Murat Demirbas, Leslie Lamport and Chris Newcombe, the AWS engineer who brought TLA+ to Amazon. Tooling projects may run under their own technical bodies: in 2026 Apalache, the symbolic model checker, became “Apalache a Series of LF Projects, LLC” with its own charter, and its README says it “has moved to TLA+ Foundation”.

For someone choosing a technology, the badge covers the TLA+ language and the tools in the tlaplus GitHub organisation (the SANY parser, the TLC model checker, the PlusCal translator, the TLAPS proof system, the VS Code extension, CommunityModules and the Examples), plus Apalache. It doesn’t cover the many other formal methods tools such as P, Alloy or Lean. There are no maturity stages: a project is part of the foundation or it isn’t. The foundation is small, with three paying members, and much of the tool work rests on a few maintainers and the grants it pays for.

Its projects in this catalog

TLA+Open sourceLeslie Lamport’s language for specifying concurrent and distributed systems as simple mathematics, with tools that check the designs: the TLC and Apalache model checkers and the TLAPS proof system.

In depth

What the money pays for#

The charter’s job for the fund is to spend dues on TLA+. In practice that has meant grants, prizes and events.

Grant programme

since 2024

Proposals for $1,000 to $100,000, normally finished within a year. The first call opened in July 2024 and the programme is now rolling. Funded so far: Andrew Helwer, $93,000 to unify the tools on one parser, SANY, including moving TLAPS onto it; Ian Dardik and Eunsuk Kang, $42,000 for compositional inference of inductive invariants, used to verify a Raft specification from MongoDB; and Karolis Petrauskas, $12,800 for proof decomposition in the VS Code extension.

GenAI-accelerated TLA+ challenge

2025

A prize challenge for using AI with TLA+, with submissions due July 3, 2025 under MIT. First place, an NVIDIA GeForce RTX 5090 sponsored by NVIDIA, went to Specula, which derives TLA+ specifications from source code and was shown on etcd’s Raft; the foundation gave GitHub Copilot seats to the runners-up.

Community events and updates

yearly

Annual TLA+ community events, most recently on April 12, 2026 alongside ETAPS in Turin, plus occasional industry conferences. From December 2024 to August 2025 the foundation’s blog carried monthly development updates covering TLC, Apalache, TLAPS, SANY and the VS Code extension.

Who decides#

The Governing Board manages the fund: it approves the budget, elects a chair and a treasurer, approves new technical projects together with the Technical Advisory Council (TAC), and handles outreach and legal matters with the LF. Its voting members are one representative of each Premier member, the elected General member representatives and the TAC’s chair; no company may hold more than two seats. Board meetings are private unless the board decides otherwise. The published minutes of the May 28, 2024 meeting list three board members: Chris Newcombe for Oracle, Leslie Lamport for Microsoft and julia ferraioli for AWS.

Decisions about the language belong to the SLC under the TLA+ technical charter. Its meetings are meant to be open to the public; it aims for consensus, and when it votes, half its voting members make a quorum and a majority of those present decides. It approves sub-projects, releases and contribution rules, and anyone can become a committer by a majority vote of the existing committers. When the foundation was created, Lamport wrote that it is “henceforth responsible for determining what the TLA+ language is and will be”; in August 2024 he, Merz and Newcombe set out the board’s view of which language changes should and shouldn’t be considered.

Where it came from2021–2026

For more than two decades TLA+ was looked after by its creator, Leslie Lamport, with support from Microsoft, where he worked at Microsoft Research. By 2021 it had industrial users at AWS, Microsoft, Intel and elsewhere, but no foundation of its own. In October 2021 a group of TLA+ people met to plan a foundation: they heard from Simon Peyton Jones about the Haskell Foundation, from Florian Gilcher about the Rust Foundation, and from the Microsoft Open Source Office, which recommended joining the Linux or Eclipse foundations rather than building one from scratch. By December the minutes say the Linux Foundation “sounds best”, and in March 2022 the group had contacted the LF.

The TLA+ Project became a series of LF Projects on January 5, 2023, the foundation’s charter took effect on January 10, and the LF announced the TLA+ Foundation on April 21, 2023, with AWS, Microsoft and Oracle as members. Its launch statement said it would fund education, research and tools and act as a language committee. In July 2024 it opened its first call for grant proposals, and in August Lamport wrote that “the future of TLA+ is now in the hands of the TLA+ Foundation”.

Lamport retired from Microsoft on January 3, 2025, and by April Microsoft no longer appeared among the members. The foundation carried on with grants, monthly development updates and, in 2025, a challenge on using generative AI with TLA+, whose prizes NVIDIA helped fund. In 2026 Apalache, developed at TU Wien and Informal Systems since 2016, became the foundation’s second project, and in July NVIDIA joined AWS and Oracle as a member.

Why it’s built this way

Join the Linux Foundation instead of building a new foundation
The Microsoft Open Source Office advised joining the Linux or Eclipse foundation, both tax-exempt and based in the US, rather than starting from scratch; the planners settled on the LF, noting that Eclipse requires ownership of the code’s copyright.
A fund for the money, project series for the code
The directed fund raises and spends dues under a Governing Board, while TLA+ and Apalache each sit in their own LF Projects series with a technical charter, so paying members don’t control the language.
A language committee, not a technical steering committee
TLA+ is first of all a language, so its charter gives oversight to a Specification Language Committee that started with Lamport, Merz, Demirbas and Newcombe, and lets tooling projects run under their own bodies.
Spend on grants
With few full-time maintainers, the foundation turns dues into fixed-scope grants of up to $100,000, such as the work to move TLAPS onto the shared SANY parser.

Timeline

  1. 2021

    Planning meetings for a TLA+ foundation start in October

  2. 2022

    The group settles on the Linux Foundation and contacts it in March

  3. 2023

    Technical charter adopted January 5; the LF announces the TLA+ Foundation on April 21

  4. 2024

    First grant call in July; Lamport hands the future of TLA+ to the foundation in August

  5. 2025

    Lamport retires from Microsoft on January 3; Microsoft leaves the member list; GenAI-accelerated TLA+ challenge

  6. 2026

    Apalache becomes a foundation project; NVIDIA joins as a member in July

Sources · facts checked 2026-10-28

Improve this page on GitHub