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-images.s3.amazonaws.com/shared/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: DomainSecurity
  url: security/tla-plus-foundation-domain-security.yml
- 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:support@tlapl.us
- 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: kin@apievangelist.com