A gently curated list of companies using verification formal methods in industry
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
An instructional website with progressively worked examples of TLA+ specifications and model checking.
TLA+ specification of Flexible Paxos
Synchronous fault-tolerant distributed algorithms encoded in TLA+
TLA+ specification for Succinct Atomic Swap smart contract
TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus
A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+
Model Checking for Industrial Programmers with TLA+
TLA+ specification of Fast Flexible Paxos
The TLA+ Video Course by Leslie Lamport
Some examples and notes while learning TLA+ modeling language.
📜 WIP Hop Protocol TLA+ Specification
A collection of various TLA+ examples and helper functions for learning.
TLA+ specification of a TCP/IP 3-way handshake in multi-client environment.
TLA+ specification of the parser for BIP32 path templates
TLA Specification for the "Wolf, goat, and cabbage" puzzle (https://en.wikipedia.org/wiki/Wolf,_goat_and_cabbage_problem)
Markdown to LaTeX
Version Gate is a standalone service for coordinating coherent writes and reads across distributed data. It assigns ordered coordinator versions, prevents incompatible live operations from overlapping, and can also maintain immutable snapshots as an optional secondary capability.
To associate your repository with the tla-specification topic, visit your repo's landing page and select "manage topics."