Here are
72 public repositories
matching this topic...
TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
Updated
Jun 24, 2022
Java
writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+
Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
APALACHE: symbolic model checker for TLA+
Updated
Jul 8, 2022
Scala
Command line binaries for the TLA+ language
Updated
May 7, 2022
Shell
PGo is a source to source compiler from Modular PlusCal specs into Go programs.
Updated
Mar 16, 2021
Python
Python interpreter for TLA+ specifications
Updated
May 12, 2021
Python
A simple REPL for the TLA+ language, using the TLC model checker.
Updated
Jun 25, 2020
Python
Proving a blocking queue deadlock free in a dozen different ways
Updated
Jun 2, 2021
Dafny
Updated
Jul 6, 2022
Python
TLA+ specification of Flexible Paxos
Utilities for the TLA+ ecoystem and model-based testing using TLA+.
Updated
Jun 9, 2022
Python
Different TLA+ specifications, mostly for learning purposes
Updated
Nov 11, 2021
Emacs Lisp
Convert TLA+ output (and values) into JSON
Updated
Mar 3, 2021
Scala
TLA+ specification for Succinct Atomic Swap smart contract
Specifying and Verifying the consensus algorithm in PaxosStore using TLA+
TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus
TLA+ questions, answers, and experiments
How to use TLA+ / TLA+ specification of the ClickHouse replication protocol
A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+
Temporal Logic of Actions Modeling for Python
Updated
Mar 27, 2021
Python
Lightning talk about TLA+ for Scala Exchange 2018
Updated
Jan 6, 2020
Jupyter Notebook
Formal models of vac protocols
The TLA+ Video Course by Leslie Lamport
Updated
Oct 27, 2021
HTML
Improve this page
Add a description, image, and links to the
tla
topic page so that developers can more easily learn about it.
Curate this topic
Add this topic to your repo
To associate your repository with the
tla
topic, visit your repo's landing page and select "manage topics."
Learn more
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session.
You signed out in another tab or window. Reload to refresh your session.
The
TlaDocumentSymbolsProviderstumbles on operators while parsing constants and doesn't report them as model symbols. As a result, const operator names don't appear in the outline panel and in completion suggestions. Such operators also prevent parsing of the following constants.A simple case:
Neither
FoonorBarmakes it to the model symbols list