TLA Plus Foundation

TLC Model Checker

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.

GitHub

Documentation

📖
Documentation
https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/executing-tlc.html

SDKs

📦
GitHubRepository
https://github.com/tlaplus/tlaplus

API entry from apis.yml

apis.yml Raw ↑ 
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