Repositories list

• tlaplus

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

  javaalgorithmshigh-performance+ 5verificationspecificationsmodel-checkingmit-licensetla

  Java

  •

  MIT License

  •222•2.5k•272•31•Updated Aug 15, 2025Aug 15, 2025

• vscode-tlaplus

  Public
  TLA+ language support for Visual Studio Code

  verificationspecificationvscode-extension+ 5model-checkingformal-methodstlatlcpluscal

  TypeScript

  •

  MIT License

  •41•388•57•6•Updated Aug 15, 2025Aug 15, 2025

• foundation

  Public
  TLA+ Foundation

  HTML

  •5•30•2•1•Updated Aug 13, 2025Aug 13, 2025

• TLAiBench

  Public
  TLA

  •2•8•0•0•Updated Aug 13, 2025Aug 13, 2025

• Examples

  Public
  A collection of TLA⁺ specifications of varying complexities.

  pluscaltlaplus

  TLA

  •

  Other

  •210•1.4k•13•1•Updated Aug 9, 2025Aug 9, 2025

• tlapm

  Public
  The TLA⁺ Proof Manager

  OCaml

  •

  BSD 2-Clause "Simplified" License

  •24•83•54•7•Updated Aug 1, 2025Aug 1, 2025

• devkit

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

  Java

  •

  MIT License

  •0•2•0•0•Updated Jun 20, 2025Jun 20, 2025

• CommunityModules

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

  pluscaltlaplustla-specification

  TLA

  •

  MIT License

  •41•289•13•4•Updated May 15, 2025May 15, 2025

• conf

  Public
  CSS

  •

  Creative Commons Attribution 4.0 International

  •1•0•0•0•Updated May 8, 2025May 8, 2025

• tlaplus-standard

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

  TLA

  •

  MIT License

  •1•5•1•0•Updated Mar 19, 2025Mar 19, 2025

• rfcs

  Public
  RFCs for changes to the TLA+ specification language

  TLA

  •

  MIT License

  •1•12•16•0•Updated Mar 19, 2025Mar 19, 2025

• azure-cosmos-tla

  Public
  Azure Cosmos TLA+ specifications

  azuremodel-checkingcosmosdb+ 1tlaplus

  TLA

  •

  MIT License

  •43•22•4•0•Updated Jan 21, 2025Jan 21, 2025

• lecture

  Public
  The TLA+ Video Course by Leslie Lamport

  tlatla-plustlaplus+ 1tla-specification

  HTML

  •

  Other

  •3•10•0•0•Updated Dec 31, 2024Dec 31, 2024

• PlusCalCheatSheet

  Public
  PlusCal Cheat Sheet by Stephan Merz

  TeX

  •

  MIT License

  •2•23•0•0•Updated Sep 27, 2024Sep 27, 2024

• awesome-tlaplus

  Public
  A curated list of TLA+ resources.

  25•151•2•0•Updated Jun 22, 2024Jun 22, 2024

• PlusPy

  Public
  Python interpreter for TLA+ specifications

  pythoninterpretertla

  Python

  •

  MIT License

  •14•114•1•0•Updated Jun 2, 2024Jun 2, 2024

• patterns

  Public
  MIT License

  •0•7•1•0•Updated Feb 13, 2024Feb 13, 2024

• Survey

  Public
  Results TLA+ Surveys

  Creative Commons Zero v1.0 Universal

  •0•2•0•0•Updated May 19, 2022May 19, 2022

• DrTLAPlus

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

  pluscaltlaplusalgorithm+ 1protocol

  TLA

  •100•837•0•0•Updated Apr 18, 2022Apr 18, 2022

• ConcurrentSCC

  Public
  Prototypes of Concurrent Strongly Connected Components (SCC) algorithms

  algorithmstarjanscc+ 2concurrenttlaplus

  Java

  •

  MIT License

  •0•1•0•0•Updated Apr 14, 2022Apr 14, 2022

• www

  Public
  http://www.tlapl.us

  HTML

  •

  MIT License

  •1•1•0•1•Updated Aug 10, 2021Aug 10, 2021

• tlapm_alternative_parser_experiment

  Public archive
  The rewrite of TLAPM, the TLAPS proof manager

  OCaml

  •

  Other

  •0•0•18•1•Updated Jul 23, 2019Jul 23, 2019