# quint-co/quint

An executable specification language  with delightful tooling based on the temporal logic of actions (TLA)

Repository: https://github.com/quint-co/quint
Canonical: https://ross.abutalabs.com/products/quint
Homepage: https://quint.sh
Language: TypeScript
License: Apache-2.0
License Family: permissive
Topics: language, tlaplus, quint, apalache, specification, formal-methods, verification, specification-language
Last push: 2026-08-20T13:55:29+00:00

## Health v2 (maintenance only)
Score: 91/100 (v2, computed 2026-09-02T17:46:02.011165+00:00)
- activity 98, release rhythm 77, longevity 100
- inputs: {"age_days": 1923, "days_push": 13, "days_rel": 155, "gap_med": 19.0, "n_releases_24m": 25}
- flags: none
- formula: round(0.45*activity + 0.35*rhythm + 0.20*longevity); archived -> min(score, 10)

## Adoption (not part of the score)
Stars 1638, forks 143 (observed 2026-08-28T04:05:15.053145+00:00)

## What it is
Quint is an executable specification language based on the Temporal Logic of Actions (TLA+), designed for modeling and verifying the behavior of systems and protocols. It ships with a CLI, REPL, simulator, and integration with the Apalache model checker, letting teams run and verify specs to catch design bugs before implementation.

## Use cases
- write executable specifications for distributed systems
- verify protocol invariants before implementation
- find subtle concurrency bugs with model checking
- generate model-based tests from a system spec
- simulate system designs in a REPL
- modern alternative to TLA+ for formal methods

## When to choose
- designing consensus protocols or security-critical distributed systems
- you want runnable, verifiable specs instead of static design documents
- you prefer a modern, developer-friendly syntax over raw TLA+
- you need model-based testing derived from a specification

## When to avoid
- you need a general-purpose programming language to build applications
- your team has no appetite for formal specification and verification
- you only need lightweight unit or integration testing of existing code

## Facets
- artifact type: cli-tool
- maturity: active
- function: programming-language, interpreter, cli, testing, simulation
- domain: programming-languages, microservices, developer-tools
- platform: cli, cross-platform
- tags: specification-language, tla-plus, formal-verification, model-checking, model-based-testing, apalache, temporal-logic, repl, verification, formal-methods, algorithms, nodejs

## Member repositories
- quint-co/quint (main) score 91

## Provenance
- Observed fields: from GitHub, fetched 2026-08-28T04:05:15.053145+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-30T03:46:38.836447+00:00, confidence not recorded.
  - readme: https://github.com/quint-co/quint (fetched 2026-08-28T04:05:15.053145+00:00, sha 0fd6370e4096)
  - homepage: https://quint.sh (fetched 2026-08-29T11:20:04.048251+00:00, sha 69f8c26d828f)
  - site_page: https://quint.sh/docs/language-basics (fetched 2026-08-29T11:20:04.069409+00:00, sha 677fdb3ad0a9)
  - site_page: https://quint.sh/docs/getting-started (fetched 2026-08-29T11:20:04.057412+00:00, sha 9b87af42493f)
  - site_page: https://quint.sh/about (fetched 2026-08-29T11:20:04.059322+00:00, sha f4215dc71e42)
  - site_page: https://quint.sh/docs/why (fetched 2026-08-29T11:20:04.063781+00:00, sha c86815c19ade)
  - site_page: https://quint.sh/docs/what-does-quint-do (fetched 2026-08-29T11:20:04.065614+00:00, sha e1862012d230)
  - site_page: https://quint.sh/docs/use-cases (fetched 2026-08-29T11:20:04.067405+00:00, sha 782bccfa986c)
  - site_page: https://quint.sh/docs/lessons (fetched 2026-08-29T11:20:04.071487+00:00, sha 2636f95debf1)
  - site_page: https://quint.sh/faq (fetched 2026-08-29T11:20:04.061063+00:00, sha f7a798bb2b51)
- Data as of 2026-08-30T08:39:29.467469+00:00.