# tlaplus/tlaplus

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

Repository: https://github.com/tlaplus/tlaplus
Canonical: https://ross.abutalabs.com/products/tlaplus
Homepage: https://www.tlapl.us
Language: Java
License: MIT
License Family: permissive
Topics: tla, specifications, model-checking, verification, high-performance, java, algorithms, mit-license
Last push: 2026-08-21T16:14:06+00:00

## Health v2 (maintenance only)
Score: 85/100 (v2, computed 2026-09-02T17:46:02.011165+00:00)
- activity 98, release rhythm 60, longevity 100
- inputs: {"age_days": 3865, "days_push": 12, "days_rel": 12, "gap_med": null, "n_releases_24m": 1}
- flags: prerelease_only
- formula: round(0.45*activity + 0.35*rhythm + 0.20*longevity); archived -> min(score, 10)

## Adoption (not part of the score)
Stars 3018, forks 263 (observed 2026-08-28T04:07:38.413568+00:00)

## What it is
The official TLA+ tools repository containing TLC, a model checker for TLA+ specifications, plus the SANY parser, PlusCal translator, REPL, and the Eclipse-based Toolbox IDE. TLA+ is a formal specification language for modeling concurrent and distributed systems to find design errors before implementation.

## Use cases
- model check a distributed system design for liveness and safety violations
- verify concurrent algorithms before writing code
- formally specify a protocol and explore its state space
- translate PlusCal algorithms to TLA+ specifications
- find race conditions and deadlocks in a system design

## When to choose
- you need to rigorously verify the design of concurrent or distributed systems
- you want to catch fundamental design errors before implementation
- you are modeling safety-critical systems where correctness matters
- you want a mature, actively maintained model checker backed by the TLA+ Foundation

## When to avoid
- you want unit testing of existing code rather than design-level verification
- your team cannot invest in learning a mathematical specification language
- you need lightweight property testing of implementations instead of exhaustive model checking
- you require a GUI IDE - the Toolbox is unmaintained; prefer the VS Code extension

## Facets
- artifact type: application
- maturity: active
- function: testing, cli, developer-tools, simulation, parser, interpreter
- domain: developer-tools, microservices, programming-languages
- platform: jvm, cross-platform, cli
- tags: tla-plus, model-checking, formal-verification, formal-methods, specification-language, pluscal, concurrency, distributed-systems, ide, algorithms, verification

## Member repositories
- tlaplus/tlaplus (main) score 85

## Provenance
- Observed fields: from GitHub, fetched 2026-08-28T04:07:38.413568+00:00.
- Health v2: computed from the inputs above; adoption is never an input.
- Inferred fields (summary, facets, guidance): AI-extracted, prompt v1, taxonomy v1, on 2026-08-30T07:30:02.943099+00:00, confidence not recorded.
  - readme: https://github.com/tlaplus/tlaplus (fetched 2026-08-28T04:07:38.413568+00:00, sha 153da3c4bf8b)
  - homepage: https://www.tlapl.us (fetched 2026-08-29T09:45:16.084144+00:00, sha a8a0c81afc9a)
- Data as of 2026-08-30T08:39:29.467469+00:00.