tlaplus
There are 118 repositories under tlaplus topic.
tlaplus/Examples
A collection of TLA⁺ specifications of varying complexities
informalsystems/quint
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
tlaplus/DrTLAPlus
Dr. TLA+ series - learn an algorithm and protocol, study a specification
ligurio/practical-fm
A gently curated list of companies using verification formal methods in industry
lemmy/BlockingQueue
Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
apalache-mc/apalache
APALACHE: symbolic model checker for TLA+ and Quint
tlaplus/CommunityModules
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
hwayne/learntla-v2
Learn TLA+ for free! No prior experience necessary!
afonsonf/tlaplus-graph-explorer
A static web application to explore and animate a TLA+ state graph.
fizzbee-io/fizzbee
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
hwayne/tlacli
A script for running TLA+/TLC from the command line
informalsystems/atomkraft
Advanced fuzzing via Model Based Testing for Cosmos blockchains
will62794/tla-web
Interactive, web-based environment for exploring and visualizing TLA+ specifications.
eras/tlsd
Generate (message) sequence diagrams from TLA+ state traces
OliverKillane/Imperial-Computing-Notes
A selection of textbook-like course notes for the Imperial College Computing modules.
tlaplus-community/tree-sitter-tlaplus
A tree-sitter grammar for TLA⁺ and PlusCal
informalsystems/modelator
Model-based testing tool
tlaplus-workshops/ewd998
Distributed termination detection on a ring, due to Shmuel Safra:
lorin/tla-linearizability
Reading the linearizability paper with TLA+
will62794/tlaplus_animation
A TLA+ module for animating TLC traces.
lemmy/lets-prove-blocking-queue
Proving a blocking queue deadlock free in a dozen different ways
JYwellin/CRDT-TLA
Specifying and Verifying CRDT Protocols using TLA+
lemmy/ewd998
Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF
pascalpoizat/fbpmn
:microscope: formal tools for BPMN
istoilkovska/synchronous-tla-benchmarks
Synchronous fault-tolerant distributed algorithms encoded in TLA+
mryndzionek/tlaplus_specs
Different TLA+ specifications, mostly for learning purposes
mrc/tla-tools
TLA+ tools for Emacs
informalsystems/modelator-py
Utilities for the TLA+ ecoystem and model-based testing using TLA+.
ret/specifica
Basic TLA+ related Haskell libraries (parser, evaluator, pretty-printer)
dgpv/SASwap_TLAplus_spec
TLA+ specification for Succinct Atomic Swap smart contract
cwi-swat/tla-ci
TLA+ specifications accompanying paper: Automated Validation of State-Based Client-Centric Isolation with TLA+. (https://doi.org/10.1007/978-3-030-67220-1_4) Based on Crooks' Isolation (https://dl.acm.org/doi/10.1145/3087801.3087802).
japgolly/tla2json
Convert TLA+ output (and values) into JSON
informalsystems/tla-apalache-workshop
Material for a workshop on Apalache and TLA+. To be populated with more examples.
Isaac-DeFrain/TLAplusFun
TLA+ questions, answers, and experiments
tezedge/tezedge-specification
TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus
tlaplus/azure-cosmos-tla
Azure Cosmos TLA+ specifications