TLA Plus Foundation

aid: tla-plus-foundation
name: TLA Plus Foundation
description: >-
  The TLA+ Foundation is an independent nonprofit hosted by the Linux Foundation,
  dedicated to fostering the adoption of the TLA+ specification language in industry,
  academia, and education. Created by Leslie Lamport, TLA+ is a high-level formal
  specification language based on set theory and temporal logic for modeling concurrent
  and distributed systems. Inaugural members include Amazon Web Services (AWS) and
  Oracle. The Foundation funds research and development, maintains the TLC model
  checker, TLAPS proof system, and TLA+ Toolbox IDE, and coordinates community
  resources including the VS Code extension, CommunityModules, and formal verification
  examples. The current stable release is v1.7.4 (The Xenophanes release).
type: Index
position: Consumer
access: 3rd-Party
image: https://kinlane-productions2.s3.amazonaws.com/apis-json/apis-json-logo.jpg
tags:
  - Formal Methods
  - Linux Foundation
  - Specifications
  - Verification
  - Distributed Systems
  - Concurrency
created: '2026-03-16'
modified: '2026-05-03'
url: >-
  https://raw.githubusercontent.com/api-evangelist/tla-plus-foundation/refs/heads/main/apis.yml
specificationVersion: '0.19'
apis:
  - aid: tla-plus-foundation:tlc-model-checker
    name: TLC Model Checker
    description: >-
      TLC is the primary model checker for specifications written in TLA+. It
      can be run from the command line using tla2tools.jar or consumed as a Java
      dependency via Maven from central.sonatype.org. Requires Java 11+. The
      current stable release is v1.7.4 (The Xenophanes release) with pre-release
      v1.8.0 (The Clarke release) available.
    humanURL: https://github.com/tlaplus/tlaplus
    tags:
      - Model Checking
      - Formal Verification
      - Java
    properties:
      - type: Documentation
        url: https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/executing-tlc.html
      - type: GitHubRepository
        url: https://github.com/tlaplus/tlaplus

  - aid: tla-plus-foundation:tlaps-proof-system
    name: TLAPS Proof System
    description: >-
      The TLA+ Proof Manager (TLAPS) is a proof system for TLA+ specifications,
      enabling formal mathematical proofs of system properties. It integrates
      with back-end provers and supports interactive proof development.
    humanURL: https://tla.msr-inria.inria.fr/tlaps/
    tags:
      - Proof System
      - Formal Verification
      - Mathematics
    properties:
      - type: Documentation
        url: https://tla.msr-inria.inria.fr/tlaps/
      - type: GitHubRepository
        url: https://github.com/tlaplus/tlapm

  - aid: tla-plus-foundation:tla-toolbox-ide
    name: TLA+ Toolbox IDE
    description: >-
      The TLA+ Toolbox is a full-featured IDE for writing TLA+ specifications,
      running TLC model checks, and managing proofs with TLAPS. Available as a
      standalone Eclipse-based application.
    humanURL: https://github.com/tlaplus/tlaplus
    tags:
      - IDE
      - Tooling
      - Development
    properties:
      - type: Documentation
        url: https://tla.msr-inria.inria.fr/tlatoolbox/doc/
      - type: GitHubRepository
        url: https://github.com/tlaplus/tlaplus

  - aid: tla-plus-foundation:vscode-tlaplus
    name: TLA+ VS Code Extension
    description: >-
      The official TLA+ extension for Visual Studio Code providing language
      support, syntax highlighting, TLC integration, and model checking from
      within the VS Code editor.
    humanURL: https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus
    tags:
      - IDE
      - VS Code
      - Tooling
    properties:
      - type: Documentation
        url: https://github.com/tlaplus/vscode-tlaplus
      - type: GitHubRepository
        url: https://github.com/tlaplus/vscode-tlaplus

  - aid: tla-plus-foundation:community-modules
    name: TLA+ Community Modules
    description: >-
      A curated collection of TLA+ snippets, operators, and modules contributed
      by the TLA+ community, providing reusable formal specification components
      for common patterns in concurrent and distributed systems.
    humanURL: https://github.com/tlaplus/CommunityModules
    tags:
      - Community
      - Modules
      - Specifications
    properties:
      - type: Documentation
        url: https://github.com/tlaplus/CommunityModules
      - type: GitHubRepository
        url: https://github.com/tlaplus/CommunityModules

  - aid: tla-plus-foundation:tlaplus-examples
    name: TLA+ Specification Examples
    description: >-
      A collection of TLA+ specifications of varying complexity covering
      distributed algorithms, consensus protocols, concurrent data structures,
      and system models. Includes reference implementations for learning and validation.
    humanURL: https://github.com/tlaplus/Examples
    tags:
      - Examples
      - Specifications
      - Learning
    properties:
      - type: Documentation
        url: https://github.com/tlaplus/Examples
      - type: GitHubRepository
        url: https://github.com/tlaplus/Examples

common:
  - type: Website
    url: https://foundation.tlapl.us/
  - type: Documentation
    url: https://lamport.azurewebsites.net/tla/tla.html
  - type: GitHubOrganization
    url: https://github.com/tlaplus
  - type: Support
    url: mailto:[email protected]
  - type: Features
    data:
      - name: TLC Model Checker
        description: Explicit-state model checker for TLA+ specifications supporting both exhaustive verification and simulation modes.
      - name: TLAPS Proof System
        description: Interactive proof manager for formally verifying TLA+ specifications against mathematical proofs.
      - name: TLA+ Toolbox IDE
        description: Eclipse-based IDE for writing, model-checking, and managing TLA+ specifications with TLAPS integration.
      - name: VS Code Extension
        description: Official Visual Studio Code extension providing TLA+ language support and TLC integration.
      - name: Community Modules
        description: Reusable TLA+ operator and module library contributed and maintained by the community.
      - name: Grant Program
        description: Foundation grants funding research and industry initiatives to advance TLA+ specification and tool adoption.
      - name: Maven Package Distribution
        description: TLA+ tools available as Maven Java dependency from central.sonatype.org for programmatic integration.
      - name: PlusPy Python Interpreter
        description: Python interpreter for executing TLA+ specifications, enabling Python-based formal modeling workflows.
  - type: UseCases
    data:
      - name: Distributed Algorithm Verification
        description: Model-check distributed consensus, replication, and coordination protocols against safety and liveness properties.
      - name: Concurrent System Specification
        description: Formally specify concurrent data structures, lock-free algorithms, and parallel systems using TLA+.
      - name: Protocol Design and Validation
        description: Use TLA+ to design and validate network protocols, database transactions, and API contracts before implementation.
      - name: Tooling Integration via Java API
        description: Embed TLC model checking in CI/CD pipelines or custom tools using the tla2tools Maven dependency.
      - name: Education and Training
        description: Use the TLA+ Toolbox, VS Code extension, and Leslie Lamport's video course to learn formal methods.
      - name: Safety and Liveness Proof
        description: Use TLAPS to produce machine-checked proofs of safety and liveness properties for critical systems.
  - type: Integrations
    data:
      - name: Amazon Web Services
        description: Founding member; AWS uses TLA+ for distributed systems design including DynamoDB and S3 protocols.
      - name: Oracle
        description: Founding member; uses TLA+ for database and distributed system specification.
      - name: Microsoft
        description: Early TLA+ adopter for Azure and distributed systems formal verification.
      - name: Visual Studio Code
        description: Official VS Code extension for TLA+ editing and model checking.
      - name: Maven Central
        description: TLA+ tools distributed as Java Maven dependency for programmatic integration.
      - name: Linux Foundation
        description: Parent organization hosting the TLA+ Foundation as an independent nonprofit project.
maintainers:
  - FN: Kin Lane
    email: [email protected]