GitHub topics: tlaplus
fizzbee-io/fizzbee
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
Language: Python - Size: 889 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 214 - Forks: 13
informalsystems/quint
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Language: TypeScript - Size: 65 MB - Last synced at: 2 days ago - Pushed at: 12 days ago - Stars: 922 - Forks: 48
will62794/spectacle
Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+.
Language: JavaScript - Size: 27.8 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 117 - Forks: 8
informalsystems/atomkraft
Advanced fuzzing via Model Based Testing for Cosmos blockchains
Language: Python - Size: 1.18 MB - Last synced at: about 18 hours ago - Pushed at: about 2 years ago - Stars: 83 - Forks: 10
tlaplus/DrTLAPlus
Dr. TLA+ series - learn an algorithm and protocol, study a specification
Language: TLA - Size: 21.7 MB - Last synced at: 7 days ago - Pushed at: about 3 years ago - Stars: 830 - Forks: 99
apalache-mc/apalache
APALACHE: symbolic model checker for TLA+ and Quint
Language: Scala - Size: 62.2 MB - Last synced at: 5 days ago - Pushed at: 11 days ago - Stars: 456 - Forks: 42
tlaplus/Examples
A collection of TLA⁺ specifications of varying complexities.
Language: TLA - Size: 25.6 MB - Last synced at: 14 days ago - Pushed at: 27 days ago - Stars: 1,341 - Forks: 206
tlaplus/CommunityModules
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
Language: TLA - Size: 6.38 MB - Last synced at: 15 days ago - Pushed at: about 1 month ago - Stars: 282 - Forks: 39
VadimPlh/Arrival
How to use TLA+ / TLA+ specification of the ClickHouse replication protocol
Language: TLA - Size: 808 KB - Last synced at: 2 days ago - Pushed at: almost 6 years ago - Stars: 16 - Forks: 3
hwayne/tlacli
A script for running TLA+/TLC from the command line
Language: Python - Size: 2.7 MB - Last synced at: 17 days ago - Pushed at: about 4 years ago - Stars: 80 - Forks: 4
ligurio/practical-fm
A gently curated list of companies using verification formal methods in industry
Size: 122 KB - Last synced at: 12 days ago - Pushed at: 2 months ago - Stars: 526 - Forks: 42
tlaplus/ConcurrentSCC
Prototypes of Concurrent Strongly Connected Components (SCC) algorithms
Language: Java - Size: 13.5 MB - Last synced at: 14 days ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 0
informalsystems/modelator
Model-based testing tool
Language: Python - Size: 334 MB - Last synced at: about 18 hours ago - Pushed at: about 2 months ago - Stars: 56 - Forks: 5
ret/specifica
Basic TLA+ related Haskell libraries (parser, evaluator, pretty-printer)
Language: Haskell - Size: 9.85 MB - Last synced at: 5 days ago - Pushed at: over 2 years ago - Stars: 27 - Forks: 2
mrc/tla-tools
TLA+ tools for Emacs
Language: Emacs Lisp - Size: 93.8 KB - Last synced at: 25 days ago - Pushed at: 4 months ago - Stars: 33 - Forks: 8
s12f/tlads
TLA+ and Distributed/Discrete Systems.
Language: TLA - Size: 82 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 3 - Forks: 0
tlaplus-community/tree-sitter-tlaplus
A tree-sitter grammar for TLA⁺ and PlusCal
Language: C - Size: 57.7 MB - Last synced at: 1 day ago - Pushed at: about 2 months ago - Stars: 62 - Forks: 13
Isaac-DeFrain/TLAplusFun
TLA+ questions, answers, and experiments
Language: TLA - Size: 3.39 MB - Last synced at: 25 days ago - Pushed at: over 2 years ago - Stars: 23 - Forks: 0
mmhristov/Erlaplus
Erla+ is a compiler that transpiles PlusCal specs into Erlang implementations
Language: Java - Size: 29 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 3 - Forks: 0
will62794/tlaplus_animation
A TLA+ module for animating TLC traces.
Language: TLA - Size: 56.6 KB - Last synced at: 25 days ago - Pushed at: 5 months ago - Stars: 46 - Forks: 3
lemmy/BlockingQueue
Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
Language: TLA - Size: 18.3 MB - Last synced at: 19 days ago - Pushed at: 6 months ago - Stars: 491 - Forks: 22
hwayne/learntla-v2
Learn TLA+ for free! No prior experience necessary!
Language: TLA - Size: 2.14 MB - Last synced at: about 2 months ago - Pushed at: 2 months ago - Stars: 209 - Forks: 43
manifoldfinance/tla-spec
tla++ proofs and verifications
Language: TLA - Size: 3.82 MB - Last synced at: 7 days ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0
tlaplus/azure-cosmos-tla Fork of Azure/azure-cosmos-tla
Azure Cosmos TLA+ specifications
Language: TLA - Size: 1.28 MB - Last synced at: about 1 month ago - Pushed at: 3 months ago - Stars: 21 - Forks: 5
tlaplus/lecture
The TLA+ Video Course by Leslie Lamport
Language: HTML - Size: 74.2 KB - Last synced at: about 2 months ago - Pushed at: 4 months ago - Stars: 9 - Forks: 3
japgolly/tla2json
Convert TLA+ output (and values) into JSON
Language: Scala - Size: 87.9 KB - Last synced at: 19 days ago - Pushed at: about 4 years ago - Stars: 26 - Forks: 2
FedericoPonzi/tlaplus-wiki 📦
Moved to dokuwiki: https://docs.tlapl.us
Language: CSS - Size: 852 KB - Last synced at: about 1 month ago - Pushed at: 7 months ago - Stars: 1 - Forks: 0
hengxin/tlaps-examples
Examples for TLAPS (TLA+ Proof System)
Language: TeX - Size: 4.76 MB - Last synced at: 2 months ago - Pushed at: almost 5 years ago - Stars: 13 - Forks: 6
statechannels/tla-specs
TLA+ specifications of various protocols used by wallets in the nitro protocol.
Language: TLA - Size: 396 KB - Last synced at: about 2 months ago - Pushed at: almost 5 years ago - Stars: 18 - Forks: 1
rnbguy/tla-playground
Online playground for TLA+
Language: TypeScript - Size: 116 KB - Last synced at: about 18 hours ago - Pushed at: 5 months ago - Stars: 5 - Forks: 0
informalsystems/modelator-py
Utilities for the TLA+ ecoystem and model-based testing using TLA+.
Language: Python - Size: 68.7 MB - Last synced at: 24 days ago - Pushed at: over 2 years ago - Stars: 29 - Forks: 3
pascalpoizat/fbpmn
:microscope: formal tools for BPMN
Language: Haskell - Size: 35.8 MB - Last synced at: 2 days ago - Pushed at: about 1 year ago - Stars: 35 - Forks: 6
lemmy/lets-prove-blocking-queue
Proving a blocking queue deadlock free in a dozen different ways
Language: Dafny - Size: 123 KB - Last synced at: about 1 month ago - Pushed at: 6 months ago - Stars: 43 - Forks: 5
will62794/snapshot-isolation-spec
A formal specification of snapshot isolation.
Language: TLA - Size: 78.1 KB - Last synced at: 25 days ago - Pushed at: 5 months ago - Stars: 18 - Forks: 2
afonsonf/tlaplus-graph-explorer
A static web application to explore and animate a TLA+ state graph.
Language: JavaScript - Size: 5.76 MB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 197 - Forks: 2
Isaac-DeFrain/node-debugger
Interactive node simulator for TLA+ specification of Tezos p2p
Language: OCaml - Size: 67.4 KB - Last synced at: 25 days ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0
hengxin/tla2tex
TLA+ Code to TeX Code using tla2tools.jar
Language: TeX - Size: 7.1 MB - Last synced at: 2 months ago - Pushed at: over 2 years ago - Stars: 9 - Forks: 1
oxarbitrage/zcash-p2p-spec
Modelling the Zcash P2P network
Language: TLA - Size: 1.49 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0
dgpv/ABL_contract_TLAplus_spec
TLA+ Specification for Asset-Based Lending smart contract state transition table generation
Language: TLA - Size: 3.06 MB - Last synced at: 1 day ago - Pushed at: over 4 years ago - Stars: 4 - Forks: 4
konnov/apalache-examples
Examples of efficiently using Apalache
Language: TLA - Size: 1.43 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 3 - Forks: 0
lorin/tla-linearizability
Reading the linearizability paper with TLA+
Language: TLA - Size: 224 KB - Last synced at: about 2 months ago - Pushed at: about 3 years ago - Stars: 48 - Forks: 4
smheidrich/tlaplus-state-graph-utils.py
Transform GraphViz dot files produced by TLA+
Language: Python - Size: 108 KB - Last synced at: 1 day ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0
johnyf/tlapy
Python utilities for working with TLA+ specifications
Language: Python - Size: 13.7 KB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 0
talex5/spec-vchan
A TLA+ specification for the Xen vchan protocol
Language: TLA - Size: 111 KB - Last synced at: 23 days ago - Pushed at: over 6 years ago - Stars: 15 - Forks: 0
hop-protocol/tla-spec 📦
📜 WIP Hop Protocol TLA+ Specification
Language: TLA - Size: 388 KB - Last synced at: 6 days ago - Pushed at: almost 4 years ago - Stars: 8 - Forks: 1
apalache-mc/apalache-tests
Benchmarks for apalache
Language: SMT - Size: 540 KB - Last synced at: 9 months ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 2
konnov/tlaki
TLAki: Little cute typed definitions in TLA+
Language: TLA - Size: 9.77 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 4 - Forks: 0
mryndzionek/tlaplus_specs
Different TLA+ specifications, mostly for learning purposes
Language: TLA - Size: 161 MB - Last synced at: 2 months ago - Pushed at: 12 months ago - Stars: 31 - Forks: 1
raydog99/PlusCal
TLA+ verification of distributed systems
Language: TLA - Size: 13.7 KB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0
freespek/solarkraft
Solakraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache
Language: TypeScript - Size: 11.4 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 9 - Forks: 0
VedantPimpley/HandshakeSpec
TLA+ specification of a TCP/IP 3-way handshake in multi-client environment.
Size: 151 KB - Last synced at: 7 months ago - Pushed at: over 3 years ago - Stars: 5 - Forks: 0
hengxin/tlaplus-at-nju-disalg
Learning [Lamport's TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).
Language: TeX - Size: 231 MB - Last synced at: 2 months ago - Pushed at: about 3 years ago - Stars: 12 - Forks: 7
tlaplus-workshops/ewd998
Distributed termination detection on a ring, due to Shmuel Safra:
Language: TLA - Size: 1.95 MB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 46 - Forks: 47
Alexander-N/tla-specs
Language: TLA - Size: 2.42 MB - Last synced at: 7 days ago - Pushed at: over 3 years ago - Stars: 4 - Forks: 1
informalsystems/tla-apalache-workshop
Material for a workshop on Apalache and TLA+. To be populated with more examples.
Size: 115 KB - Last synced at: about 1 year ago - Pushed at: about 2 years ago - Stars: 21 - Forks: 5
OliverKillane/Imperial-Computing-Notes
A selection of textbook-like course notes for the Imperial College Computing modules.
Language: TeX - Size: 325 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 38 - Forks: 3
elh/petri-tlaplus
🕸 TLA+ specifications for Petri nets
Language: TLA - Size: 1.33 MB - Last synced at: about 1 year ago - Pushed at: almost 2 years ago - Stars: 3 - Forks: 0
miguelmota/tla-cookbook 📦
A collection of various TLA+ examples and helper functions for learning.
Size: 8.79 KB - Last synced at: about 1 year ago - Pushed at: almost 4 years ago - Stars: 7 - Forks: 0
konnov/tlaplus-highlightjs
Syntax highlighting for TLA+ in highlightjs
Language: JavaScript - Size: 8.79 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
eu90h/tla-stuff
TLA+ specs and such
Language: TLA - Size: 549 KB - Last synced at: 12 months ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
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).
Language: TLA - Size: 1.57 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 20 - Forks: 2
miguelmota/tla-learning 📦
Some examples and notes while learning TLA+ modeling language.
Size: 24.4 KB - Last synced at: about 1 year ago - Pushed at: almost 4 years ago - Stars: 9 - Forks: 0
dgpv/SASwap_TLAplus_spec
TLA+ specification for Succinct Atomic Swap smart contract
Language: TLA - Size: 1.28 MB - Last synced at: over 1 year ago - Pushed at: almost 5 years ago - Stars: 24 - Forks: 6
SwethasriKavuri/Distributed-Mutex-TLA-specs
Compared the specifications and correctness of Distributed Mutex Algorithms and compared the efficiency, max clock values, max states reached using TLA+
Language: TLA - Size: 150 KB - Last synced at: over 1 year ago - Pushed at: over 6 years ago - Stars: 0 - Forks: 0
timewinder-dev/timewinder
Temporal Logic of Actions in Rust via Starlark
Language: Starlark - Size: 397 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
timewinder-dev/timewinder-prototype
Temporal Logic of Actions Modeling for Python
Language: Python - Size: 176 KB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 11 - Forks: 1
jb567/tla-go-back-n
A TLA+ verification of the Go-Back-N ARQ protocol
Language: TLA - Size: 3.08 MB - Last synced at: over 1 year ago - Pushed at: almost 6 years ago - Stars: 2 - Forks: 1
gitcordier/tlaplus
Language: TLA - Size: 1.44 MB - Last synced at: 15 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0
changlinli/peterson-tlaplus
A TLA+ Specification of Peterson's Algorithm
Language: TLA - Size: 27.3 KB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 5 - Forks: 1
ac259/Ben-or
When a process is betrayed and sent into a limbo by a fellow process, it regains its majority and comes back for consensus.
Language: TeX - Size: 56.7 MB - Last synced at: over 1 year ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0
gitcordier/MarkdownToLaTeX
Markdown to LaTeX
Language: Python - Size: 609 KB - Last synced at: 17 days ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 1
ankagrawal/AmbryTLA
TLA+ Specification for Ambry
Language: Shell - Size: 3.17 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0
Isaac-DeFrain/model-based-trace-checking
Model-based trace-checking ✅ check the conformance of your implementation to your specification
Language: Rust - Size: 2.06 MB - Last synced at: 25 days ago - Pushed at: over 3 years ago - Stars: 5 - Forks: 0
lemmy/ewd998 📦
Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF
Language: TLA - Size: 1.61 MB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 41 - Forks: 12
suhr/advent-of-tla
AoC goals in TLA+
Language: TLA - Size: 9.77 KB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 6 - Forks: 1
tezedge/tezedge-specification
TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus
Language: TLA - Size: 3.18 MB - Last synced at: 5 months ago - Pushed at: over 3 years ago - Stars: 20 - Forks: 4
decanus/rutschblock
A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+
Language: TLA - Size: 21.5 KB - Last synced at: about 1 year ago - Pushed at: almost 5 years ago - Stars: 18 - Forks: 1
JYwellin/CRDT-TLA
Specifying and Verifying CRDT Protocols using TLA+
Language: TLA - Size: 1.01 GB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 33 - Forks: 3
d-gaston/TLA_Specifications
A collection of TLA+ specifications I've written
Language: TLA - Size: 1 MB - Last synced at: almost 2 years ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0
johnyf/latex_packages
LaTeX style-files for graphics and mathematics
Language: TeX - Size: 92.8 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
myrrc/tlaplus-conceal.vim
View unicode characters for TLA+ files
Language: Vim Script - Size: 1.95 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 0
ZhenshengLee/zsTla 📦
Learning Material for TLA+
Language: TLA - Size: 20.5 KB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 1 - Forks: 0
eras/tlsd
Generate (message) sequence diagrams from TLA+ state traces
Language: Python - Size: 95.7 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 12 - Forks: 0
lemmy/AsyncGameOfLife Fork of mryndzionek/tlaplus_specs
Asynchronous variant of Conway's Game of Life in TLA+
Language: TLA - Size: 5.72 MB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 4 - Forks: 0
gitcordier/md2latex Fork of kavinyao/md2latex
Markdown to LaTeX. Specs in TLA+
Language: Python - Size: 2.33 MB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 2 - Forks: 0
orsinium-labs/simple-tla
Collection of useful "operators" (functions) to make TLA+ easier to learn and to use
Language: TLA - Size: 19.5 KB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0
hengxin/vis-ar-formalization
Formalization of the (VIS, AR) Specification Framework for Both Transactional and Non-Transactional Consistency Models
Language: TeX - Size: 94.2 MB - Last synced at: 2 months ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0
visualzhou/tla-trace-formatter
Parse the trace of TLC output and generate HTML with better format.
Language: Python - Size: 6.84 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 6 - Forks: 1
Isaac-DeFrain/apalache-interface
Interface files for the Apalache symbolic model checker reminiscent of OCaml
Language: OCaml - Size: 12.7 KB - Last synced at: 25 days ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
hengxin/jupiter-refinement-project
Jupiter Refinement Project
Language: TeX - Size: 55.9 MB - Last synced at: 2 months ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 0
tangruize/jupiter-experiments
Language: TLA - Size: 4.23 MB - Last synced at: 2 months ago - Pushed at: about 6 years ago - Stars: 1 - Forks: 0
Double-oxygeN/Raft.tla
TLA+ Specification of Raft Consensus Algorithm
Language: TLA - Size: 47.9 KB - Last synced at: 22 days ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
Isaac-DeFrain/liveness-checking
Liveness checking state machines without storing execution traces
Language: OCaml - Size: 10.7 KB - Last synced at: 25 days ago - Pushed at: almost 4 years ago - Stars: 2 - Forks: 0
afonsonf/tlaplus-html-examples
Example usages of the HTML.tla module
Size: 5.52 MB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 2 - Forks: 0
mssabr01/ICSVerifiedSoftwareProject
A formally verified implementation of a bolt-on security device for ICS networks. Designed with TLA+ and written/proved in F*
Language: C - Size: 53.3 MB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 5 - Forks: 2
andrewhao/tuxedo-tutes
🕴🏻 Introduction to TLA+ and formal verification methods
Language: TLA - Size: 87.9 KB - Last synced at: about 1 year ago - Pushed at: about 3 years ago - Stars: 0 - Forks: 0
josedusol/PCR
TLA+ specification of the PCR parallel programming pattern.
Language: TLA - Size: 804 KB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 1
hengxin/tla-deep-into-code
Applying TLA+/TLC/TLAPS to Source Code
Size: 13.5 MB - Last synced at: 2 months ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0
polikow/bully_election
Bully election algorithm model written in TLA+ and PlusCal
Language: TLA - Size: 156 KB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
ashishnegi/learn_tlaplus
Learn TLA+ specification
Language: TLA - Size: 3.53 MB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
