Repositories list

• Examples

  Public
  A collection of TLA⁺ specifications of varying complexities.

  pluscaltlaplus

  pluscaltlaplus

  TLA

  •

  Other

  •217217 forks•1.5k1.5k stars•1212 issues•44 pull requests•Updated May 4, 2026May 4, 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

  •254254 forks•2.9k2.9k stars•200200 issues•3131 pull requests•Updated May 4, 2026May 4, 2026

• vscode-tlaplus

  Public
  TLA+ language support for Visual Studio Code

  verificationspecificationvscode-extension+ 5

  verificationspecificationvscode-extensionmodel-checkingformal-methodstlatlcpluscal

  TypeScript

  •

  MIT License

  •4848 forks•421421 stars•6666 issues•33 pull requests•Updated May 1, 2026May 1, 2026

• CommunityModules

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

  pluscaltlaplustla-specification

  pluscaltlaplustla-specification

  TLA

  •

  MIT License

  •4646 forks•311311 stars•1313 issues•22 pull requests•Updated Apr 22, 2026Apr 22, 2026

• conf

  Public
  CSS

  •

  Creative Commons Attribution 4.0 International

  •11 fork•00 stars•00 issues•00 pull requests•Updated Apr 15, 2026Apr 15, 2026

• tlapm

  Public
  The TLA⁺ Proof Manager

  OCaml

  •

  BSD 2-Clause "Simplified" License

  •3838 forks•114114 stars•6363 issues•99 pull requests•Updated Apr 14, 2026Apr 14, 2026

• foundation

  Public
  TLA+ Foundation

  HTML

  •77 forks•3333 stars•33 issues•11 pull request•Updated Mar 30, 2026Mar 30, 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.

  2727 forks•176176 stars•22 issues•00 pull requests•Updated Mar 10, 2026Mar 10, 2026

• tla-by-example

  Public
  TypeScript

  •

  Other

  •22 forks•66 stars•22 issues•00 pull requests•Updated Mar 8, 2026Mar 8, 2026

• ValidationTestSuite

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

  Python

  •

  Other

  •00 forks•55 stars•66 issues•00 pull requests•Updated Mar 1, 2026Mar 1, 2026

• TLAiBench

  Public
  TLAi+ Benchmarks

  aiverificationspecification+ 2

  aiverificationspecificationbenchmarksllm

  Python

  •

  MIT License

  •44 forks•3232 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•2626 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

  •00 forks•22 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•1111 stars•1616 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

  •4747 forks•2020 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•1313 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•2828 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•118118 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

  •9999 forks•854854 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•11 star•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