Here are
43 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
Aug 24, 2020
Java
writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+
APALACHE: symbolic model checker for TLA+
Updated
Aug 25, 2020
Scala
Updated
Dec 9, 2019
Python
Command line binaries for the TLA+ language
Updated
Apr 23, 2020
Shell
PGo is a source to source compiler to compile PlusCal into Go lang
Python interpreter for TLA+ specifications
Updated
Jun 10, 2020
Python
A simple REPL for the TLA+ language, using the TLC model checker.
Updated
Jun 25, 2020
Python
TLA+ specification of Flexible Paxos
Different TLA+ specifications, mostly for learning purposes
Updated
Aug 15, 2020
Emacs Lisp
A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+
TLA+ specification for Succinct Atomic Swap smart contract
Basic TLA+ related Haskell libraries (parser, evaluator, pretty-printer)
Updated
Aug 28, 2020
Haskell
How to use TLA+ / TLA+ specification of the ClickHouse replication protocol
Specifying and Verifying the consensus algorithm in PaxosStore using TLA+
Lightning talk about TLA+ for Scala Exchange 2018
Updated
Jan 6, 2020
Jupyter Notebook
Formal models of vac protocols
TLA+ specification of the parser for BIP32 path templates
Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.
VS Code debug adapter for the TLA+ language
Updated
Jul 4, 2017
TypeScript
Parse the trace of TLC output and generate HTML with better format.
Updated
Nov 7, 2019
Python
TLA+ model of some SAFE network stuff
TLA+ Code to TeX Code using tla2tools.jar
A TLA+ model for a clock with hours and minutes.
Updated
Mar 16, 2018
Python
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.
Register, vote, and volunteer to make an impact during U.S. 2020 elections.
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:
CONSTANT Foo(_), BarNeither
FoonorBarmakes it to the model symbols list