Repositories list

• CommunityModules

  Public
  TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

  pluscaltlaplustla-specification

  pluscaltlaplustla-specification

  TLA

  •

  MIT License

  •4848 forks•314314 stars•1313 issues•22 pull requests•Updated Sep 9, 2026Sep 9, 2026

• model-checker-hardening

  Public
  Hardening TLC and Apalache through systematic, differential, fuzz, and regression testing to improve the reliability of TLA+ model checking

  testingfuzzingtlc+ 2

  testingfuzzingtlctlaplusapalache

  Java

  •

  Apache License 2.0

  •00 forks•77 stars•2929 issues•00 pull requests•Updated Sep 9, 2026Sep 9, 2026

• tlaplus

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

  javaalgorithmshigh-performance+ 5

  javaalgorithmshigh-performanceverificationspecificationsmodel-checkingmit-licensetla

  Java

  •

  MIT License

  •264264 forks•3k3k stars•209209 issues•3030 pull requests•Updated Sep 9, 2026Sep 9, 2026

• tlapm

  Public
  The TLA⁺ Proof Manager

  OCaml

  •

  BSD 2-Clause "Simplified" License

  •4545 forks•124124 stars•6969 issues•1111 pull requests•Updated Sep 8, 2026Sep 8, 2026

• tla-by-example

  Public
  TypeScript

  •

  Other

  •55 forks•1010 stars•33 issues•11 pull request•Updated Sep 5, 2026Sep 5, 2026

• Examples

  Public
  A collection of TLA⁺ specifications of varying complexities.

  pluscaltlaplus

  pluscaltlaplus

  TLA

  •

  Other

  •223223 forks•1.6k1.6k stars•55 issues•44 pull requests•Updated Aug 31, 2026Aug 31, 2026

• vscode-tlaplus

  Public
  TLA+ language support for Visual Studio Code

  verificationspecificationvscode-extension+ 5

  verificationspecificationvscode-extensionmodel-checkingformal-methodstlatlcpluscal

  TypeScript

  •

  MIT License

  •5050 forks•435435 stars•6767 issues•22 pull requests•Updated Aug 23, 2026Aug 23, 2026

• foundation

  Public
  TLA+ Foundation

  HTML

  •77 forks•3535 stars•33 issues•11 pull request•Updated Jul 21, 2026Jul 21, 2026

• ValidationTestSuite

  Public
  Tool qualification tests and reports for the TLA+ model checker

  Python

  •

  Other

  •22 forks•66 stars•55 issues•00 pull requests•Updated May 21, 2026May 21, 2026

• conf

  Public
  CSS

  •

  Creative Commons Attribution 4.0 International

  •11 fork•00 stars•00 issues•00 pull requests•Updated May 5, 2026May 5, 2026

• tlaplus-formatter

  Public archive
  A formatter for the TLA+ language.

  Java

  •

  Apache License 2.0

  •00 forks•88 stars•44 issues•11 pull request•Updated Mar 16, 2026Mar 16, 2026

• awesome-tlaplus

  Public
  A curated list of TLA+ resources.

  2929 forks•193193 stars•22 issues•00 pull requests•Updated Mar 10, 2026Mar 10, 2026

• TLAiBench

  Public
  TLAi+ Benchmarks

  aiverificationspecification+ 2

  aiverificationspecificationbenchmarksllm

  Python

  •

  MIT License

  •44 forks•3737 stars•55 issues•00 pull requests•Updated Feb 6, 2026Feb 6, 2026

• AgentSkills

  Public
  A repository for sharing agent capabilities and expertise related to TLA+.

  MIT License

  •11 fork•3737 stars•00 issues•00 pull requests•Updated Feb 4, 2026Feb 4, 2026

• devkit

  Public
  Documents and code artifacts teaching you how to build your own TLA⁺ tools.

  Java

  •

  MIT License

  •11 fork•33 stars•00 issues•00 pull requests•Updated Dec 1, 2025Dec 1, 2025

• tlaplus-standard

  Public archive
  A collection of various standards, proposed or established, related to TLA+

  TLA

  •

  MIT License

  •11 fork•55 stars•11 issue•00 pull requests•Updated Mar 19, 2025Mar 19, 2025

• rfcs

  Public
  RFCs for changes to the TLA+ specification language

  TLA

  •

  MIT License

  •11 fork•1212 stars•1717 issues•00 pull requests•Updated Mar 19, 2025Mar 19, 2025

• azure-cosmos-tla

  Public
  Azure Cosmos TLA+ specifications

  azuremodel-checkingcosmosdb+ 1

  azuremodel-checkingcosmosdbtlaplus

  TLA

  •

  MIT License

  •5151 forks•2121 stars•44 issues•00 pull requests•Updated Jan 21, 2025Jan 21, 2025

• lecture

  Public
  The TLA+ Video Course by Leslie Lamport

  tlatla-plustlaplus+ 1

  tlatla-plustlaplustla-specification

  HTML

  •

  Other

  •33 forks•1414 stars•00 issues•00 pull requests•Updated Dec 31, 2024Dec 31, 2024

• PlusCalCheatSheet

  Public
  PlusCal Cheat Sheet by Stephan Merz

  TeX

  •

  MIT License

  •22 forks•3232 stars•00 issues•00 pull requests•Updated Sep 27, 2024Sep 27, 2024

• PlusPy

  Public
  Python interpreter for TLA+ specifications

  pythoninterpretertla

  pythoninterpretertla

  Python

  •

  MIT License

  •1414 forks•119119 stars•11 issue•00 pull requests•Updated Jun 2, 2024Jun 2, 2024

• patterns

  Public
  MIT License

  •00 forks•77 stars•11 issue•00 pull requests•Updated Feb 13, 2024Feb 13, 2024

• Survey

  Public
  Results TLA+ Surveys

  Creative Commons Zero v1.0 Universal

  •00 forks•22 stars•00 issues•00 pull requests•Updated May 19, 2022May 19, 2022

• DrTLAPlus

  Public
  Dr. TLA+ series - learn an algorithm and protocol, study a specification

  algorithmprotocolpluscal+ 1

  algorithmprotocolpluscaltlaplus

  TLA

  •100100 forks•860860 stars•00 issues•00 pull requests•Updated Apr 18, 2022Apr 18, 2022

• ConcurrentSCC

  Public
  Prototypes of Concurrent Strongly Connected Components (SCC) algorithms

  algorithmstarjanscc+ 2

  algorithmstarjansccconcurrenttlaplus

  Java

  •

  MIT License

  •00 forks•22 stars•00 issues•00 pull requests•Updated Apr 14, 2022Apr 14, 2022

• www

  Public
  http://www.tlapl.us

  HTML

  •

  MIT License

  •11 fork•11 star•00 issues•11 pull request•Updated Aug 10, 2021Aug 10, 2021

• tlapm_alternative_parser_experiment

  Public archive
  The rewrite of TLAPM, the TLAPS proof manager

  OCaml

  •

  Other

  •00 forks•00 stars•1818 issues•11 pull request•Updated Jul 23, 2019Jul 23, 2019