hwayne/learntla-v2

Learn TLA+ for free! No prior experience necessary!

Language: TLA - Size: 2.13 MB - Last synced: 5 days ago - Pushed: 5 days ago - Stars: 171 - Forks: 39

fizzbee-io/fizzbee

Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

Language: Python - Size: 362 KB - Last synced: 5 days ago - Pushed: 5 days ago - Stars: 74 - Forks: 4

tlaplus-community/tree-sitter-tlaplus

A tree-sitter grammar for TLA⁺ and PlusCal

Language: C - Size: 55 MB - Last synced: 4 days ago - Pushed: 8 days ago - Stars: 53 - Forks: 7

tlaplus/CommunityModules

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

Language: TLA - Size: 6.4 MB - Last synced: 9 days ago - Pushed: 9 days ago - Stars: 261 - Forks: 37

konnov/tlaki

TLAki: Little cute typed definitions in TLA+

Language: TLA - Size: 8.79 KB - Last synced: 11 days ago - Pushed: 12 days ago - Stars: 2 - Forks: 0

tlaplus/Examples

A collection of TLA⁺ specifications of varying complexities

Language: TLA - Size: 25.5 MB - Last synced: 13 days ago - Pushed: 13 days ago - Stars: 1,232 - Forks: 188

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: 15 days ago - Pushed: over 3 years ago - Stars: 2 - Forks: 4

mryndzionek/tlaplus_specs

Different TLA+ specifications, mostly for learning purposes

Language: TLA - Size: 144 MB - Last synced: 19 days ago - Pushed: 19 days ago - Stars: 28 - Forks: 1

informalsystems/apalache

APALACHE: symbolic model checker for TLA+ and Quint

Language: Scala - Size: 57.9 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 403 - Forks: 38

hengxin/tlaplus-pluscal-utils

Utilities for TLA+ and PlusCal

Language: TLA - Size: 1.22 MB - Last synced: about 1 month ago - Pushed: about 3 years ago - Stars: 2 - Forks: 0

afonsonf/tlaplus-graph-explorer

A static web application to explore and animate a TLA+ state graph.

Language: JavaScript - Size: 5.76 MB - Last synced: 16 days ago - Pushed: 7 months ago - Stars: 194 - Forks: 2

informalsystems/modelator

Model-based testing tool

Language: Python - Size: 334 MB - Last synced: 20 days ago - Pushed: 12 months ago - Stars: 51 - Forks: 5

hwayne/tlacli

A script for running TLA+/TLC from the command line

Language: Python - Size: 2.7 MB - Last synced: 15 days ago - Pushed: about 3 years ago - Stars: 78 - Forks: 4

informalsystems/quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

Language: TypeScript - Size: 35.2 MB - Last synced: about 1 month ago - Pushed: about 2 months ago - Stars: 580 - Forks: 29

Double-oxygeN/Raft.tla

TLA+ Specification of Raft Consensus Algorithm

Language: TLA - Size: 47.9 KB - Last synced: about 1 month ago - Pushed: almost 2 years ago - Stars: 0 - Forks: 0

freespek/solarkraft

Solakraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache

Size: 10.8 MB - Last synced: about 2 months ago - Pushed: about 2 months ago - Stars: 6 - Forks: 0

will62794/tla-web

TLA+ Web Explorer.

Language: TLA - Size: 24 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 34 - Forks: 4

tlaplus/DrTLAPlus

Dr. TLA+ series - learn an algorithm and protocol, study a specification

Language: TLA - Size: 21.7 MB - Last synced: about 1 month ago - Pushed: about 2 years ago - Stars: 778 - Forks: 97

informalsystems/atomkraft

Advanced fuzzing via Model Based Testing for Cosmos blockchains

Language: Python - Size: 1.18 MB - Last synced: 16 days ago - Pushed: about 1 year ago - Stars: 77 - Forks: 9

tlaplus-workshops/ewd998

Distributed termination detection on a ring, due to Shmuel Safra:

Language: TLA - Size: 1.95 MB - Last synced: about 1 month ago - Pushed: 8 months ago - Stars: 46 - Forks: 47

informalsystems/tla-apalache-workshop

Material for a workshop on Apalache and TLA+. To be populated with more examples.

Size: 115 KB - Last synced: about 1 month ago - Pushed: about 1 year 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: 2 months ago - Pushed: 2 months ago - Stars: 38 - Forks: 3

ligurio/practical-fm

A gently curated list of companies using verification formal methods in industry

Size: 86.9 KB - Last synced: 2 months ago - Pushed: 2 months ago - Stars: 455 - Forks: 35

hengxin/tlaps-examples

Examples for TLAPS (TLA+ Proof System)

Language: TeX - Size: 4.76 MB - Last synced: about 1 month ago - Pushed: about 4 years ago - Stars: 9 - Forks: 6

elh/petri-tlaplus

🕸 TLA+ specifications for Petri nets

Language: TLA - Size: 1.33 MB - Last synced: about 1 month ago - Pushed: 11 months ago - Stars: 3 - Forks: 0

will62794/snapshot-isolation-spec

A formal specification of snapshot isolation.

Language: TLA - Size: 34.2 KB - Last synced: 2 months ago - Pushed: almost 5 years ago - Stars: 18 - Forks: 2

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.2 MB - Last synced: 3 months ago - Pushed: 12 months ago - Stars: 474 - Forks: 20

miguelmota/tla-cookbook 📦

A collection of various TLA+ examples and helper functions for learning.

Size: 8.79 KB - Last synced: about 1 month ago - Pushed: almost 3 years ago - Stars: 7 - Forks: 0

will62794/tlaplus_animation

A TLA+ module for animating TLC traces.

Language: TLA - Size: 46.9 KB - Last synced: 2 months ago - Pushed: over 4 years ago - Stars: 43 - Forks: 3

statechannels/tla-specs

TLA+ specifications of various protocols used by wallets in the nitro protocol.

Language: TLA - Size: 396 KB - Last synced: about 2 months ago - Pushed: almost 4 years ago - Stars: 16 - Forks: 1

konnov/tlaplus-highlightjs

Syntax highlighting for TLA+ in highlightjs

Language: JavaScript - Size: 8.79 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 0 - Forks: 0

hengxin/tla-deep-into-code

Applying TLA+/TLC/TLAPS to Source Code

Size: 13.5 MB - Last synced: 4 months ago - Pushed: about 4 years ago - Stars: 0 - Forks: 0

rnbguy/tla-playground

Online playground for TLA+

Language: TypeScript - Size: 78.1 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 1 - Forks: 0

eu90h/tla-stuff

TLA+ specs and such

Language: TLA - Size: 549 KB - Last synced: 17 days ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

pascalpoizat/fbpmn

:microscope: formal tools for BPMN

Language: Haskell - Size: 35.8 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 31 - Forks: 5

tlaplus/azure-cosmos-tla Fork of Azure/azure-cosmos-tla

Azure Cosmos TLA+ specifications

Language: TLA - Size: 1.27 MB - Last synced: about 1 month ago - Pushed: 5 months ago - Stars: 17 - Forks: 5

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: about 1 month ago - Pushed: 3 months ago - Stars: 20 - Forks: 2

miguelmota/tla-learning 📦

Some examples and notes while learning TLA+ modeling language.

Size: 24.4 KB - Last synced: about 1 month ago - Pushed: almost 3 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: 7 months ago - Pushed: almost 4 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: 7 months ago - Pushed: over 5 years ago - Stars: 0 - Forks: 0

timewinder-dev/timewinder

Temporal Logic of Actions in Rust via Starlark

Language: Starlark - Size: 397 KB - Last synced: 7 months ago - Pushed: 7 months ago - Stars: 0 - Forks: 0

timewinder-dev/timewinder-prototype

Temporal Logic of Actions Modeling for Python

Language: Python - Size: 176 KB - Last synced: 7 months ago - Pushed: about 3 years ago - Stars: 11 - Forks: 1

raymonddeng99/PlusCal

TLA+ verification of some distributed protocols

Language: TLA - Size: 1000 Bytes - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 0 - Forks: 0

tlaplus/lecture

The TLA+ Video Course by Leslie Lamport

Language: HTML - Size: 73.2 KB - Last synced: about 1 month ago - Pushed: over 2 years ago - Stars: 8 - Forks: 2

VadimPlh/Arrival

How to use TLA+ / TLA+ specification of the ClickHouse replication protocol

Language: TLA - Size: 808 KB - Last synced: 9 months ago - Pushed: almost 5 years ago - Stars: 16 - Forks: 4

skhoroshavin/tla_playground

Learning and experimenting with TLA toy models

Language: TLA - Size: 229 KB - Last synced: 10 months ago - Pushed: almost 5 years ago - Stars: 0 - Forks: 0

jb567/tla-go-back-n

A TLA+ verification of the Go-Back-N ARQ protocol

Language: TLA - Size: 3.08 MB - Last synced: 10 months ago - Pushed: almost 5 years ago - Stars: 2 - Forks: 1

gitcordier/tlaplus

Language: TLA - Size: 1.44 MB - Last synced: 10 months ago - Pushed: 10 months ago - Stars: 0 - Forks: 0

changlinli/peterson-tlaplus

A TLA+ Specification of Peterson's Algorithm

Language: TLA - Size: 27.3 KB - Last synced: 10 months ago - Pushed: over 4 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: 10 months ago - Pushed: over 4 years ago - Stars: 0 - Forks: 0

gitcordier/MarkdownToLaTeX

Markdown to LaTeX

Language: Python - Size: 609 KB - Last synced: 22 days ago - Pushed: 11 months ago - Stars: 0 - Forks: 1

manifoldfinance/tla-spec

tla++ proofs and verifications

Language: TLA - Size: 3.82 MB - Last synced: 7 days ago - Pushed: almost 3 years ago - Stars: 1 - Forks: 0

japgolly/tla2json

Convert TLA+ output (and values) into JSON

Language: Scala - Size: 87.9 KB - Last synced: 11 months ago - Pushed: about 3 years ago - Stars: 21 - Forks: 2

mrc/tla-tools

TLA+ tools for Emacs

Language: Emacs Lisp - Size: 64.5 KB - Last synced: 11 months ago - Pushed: 11 months ago - Stars: 27 - Forks: 6

ret/specifica

Basic TLA+ related Haskell libraries (parser, evaluator, pretty-printer)

Language: Haskell - Size: 9.85 MB - Last synced: 9 months ago - Pushed: over 1 year ago - Stars: 24 - Forks: 2

ankagrawal/AmbryTLA

TLA+ Specification for Ambry

Language: Shell - Size: 3.17 MB - Last synced: 29 days ago - Pushed: about 1 month ago - Stars: 1 - 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: about 1 year ago - Pushed: about 1 year ago - Stars: 41 - Forks: 12

informalsystems/modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.

Language: Python - Size: 68.7 MB - Last synced: 17 days ago - Pushed: over 1 year ago - Stars: 28 - Forks: 2

suhr/advent-of-tla

AoC goals in TLA+

Language: TLA - Size: 9.77 KB - Last synced: 2 months ago - Pushed: over 2 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: 2 months ago - Pushed: over 2 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: about 1 month ago - Pushed: about 4 years ago - Stars: 18 - Forks: 1

informalsystems/apalache-tests

Benchmarks for apalache

Language: SMT - Size: 540 KB - Last synced: about 1 month ago - Pushed: about 1 year ago - Stars: 6 - Forks: 2

JYwellin/CRDT-TLA

Specifying and Verifying CRDT Protocols using TLA+

Language: TLA - Size: 1.01 GB - Last synced: about 1 year ago - Pushed: almost 3 years ago - Stars: 33 - Forks: 3

lorin/tla-linearizability

Reading the linearizability paper with TLA+

Language: TLA - Size: 224 KB - Last synced: about 1 year ago - Pushed: about 2 years ago - Stars: 28 - Forks: 4

d-gaston/TLA_Specifications

A collection of TLA+ specifications I've written

Language: TLA - Size: 1 MB - Last synced: 12 months ago - Pushed: about 1 year ago - Stars: 0 - Forks: 0

johnyf/latex_packages

LaTeX style-files for graphics and mathematics

Language: TeX - Size: 92.8 KB - Last synced: about 1 month ago - Pushed: almost 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: about 1 year ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0

Isaac-DeFrain/TLAplusFun

TLA+ questions, answers, and experiments

Language: TLA - Size: 3.39 MB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 16 - Forks: 0

ZhenshengLee/zsTla 📦

Learning Material for TLA+

Language: TLA - Size: 20.5 KB - Last synced: about 1 year ago - Pushed: about 3 years ago - Stars: 1 - Forks: 0

eras/tlsd

Generate (message) sequence diagrams from TLA+ state traces

Language: Python - Size: 95.7 KB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 12 - Forks: 0

lemmy/lets-prove-blocking-queue

Proving a blocking queue deadlock free in a dozen different ways

Language: Dafny - Size: 120 KB - Last synced: about 1 year ago - Pushed: almost 3 years ago - Stars: 37 - Forks: 5

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: about 1 year ago - Pushed: over 3 years ago - Stars: 4 - Forks: 0

Alexander-N/tla-specs

Language: TLA - Size: 2.42 MB - Last synced: 3 months ago - Pushed: over 2 years ago - Stars: 3 - Forks: 1

gitcordier/md2latex Fork of kavinyao/md2latex

Markdown to LaTeX. Specs in TLA+

Language: Python - Size: 2.33 MB - Last synced: about 1 year ago - Pushed: over 3 years ago - Stars: 2 - Forks: 0

hengxin/tla2tex

TLA+ Code to TeX Code using tla2tools.jar

Language: TeX - Size: 7.1 MB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 5 - Forks: 1

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: 4 months ago - Pushed: over 1 year 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: 2 months ago - Pushed: 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: about 1 year ago - Pushed: almost 3 years ago - Stars: 4 - Forks: 1

hop-protocol/tla-spec

📜 WIP Hop Protocol TLA+ Specification

Language: TLA - Size: 388 KB - Last synced: about 1 year ago - Pushed: almost 3 years ago - Stars: 8 - Forks: 1

talex5/spec-vchan

A TLA+ specification for the Xen vchan protocol

Language: TLA - Size: 111 KB - Last synced: about 1 year ago - Pushed: over 5 years ago - Stars: 16 - 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: about 1 year ago - Pushed: over 4 years ago - Stars: 6 - Forks: 1

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: about 1 year ago - Pushed: over 2 years ago - Stars: 10 - Forks: 7

Isaac-DeFrain/node-debugger

Interactive node simulator for TLA+ specification of Tezos p2p

Language: OCaml - Size: 67.4 KB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 1 - Forks: 0

Isaac-DeFrain/apalache-interface

Interface files for the Apalache symbolic model checker reminiscent of OCaml

Language: OCaml - Size: 12.7 KB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0

hengxin/jupiter-refinement-project

Jupiter Refinement Project

Language: TeX - Size: 55.9 MB - Last synced: about 1 year ago - Pushed: over 3 years ago - Stars: 1 - Forks: 0

tangruize/jupiter-experiments

Language: TLA - Size: 4.23 MB - Last synced: about 1 year ago - Pushed: over 5 years ago - Stars: 1 - Forks: 0

Isaac-DeFrain/liveness-checking

Liveness checking state machines without storing execution traces

Language: OCaml - Size: 10.7 KB - Last synced: about 1 year ago - Pushed: about 3 years ago - Stars: 2 - Forks: 0

tlaplus/ConcurrentSCC

Prototypes of Concurrent Strongly Connected Components (SCC) algorithms

Language: Java - Size: 13.5 MB - Last synced: about 1 month ago - Pushed: about 2 years ago - Stars: 0 - Forks: 0

afonsonf/tlaplus-html-examples

Example usages of the HTML.tla module

Size: 5.52 MB - Last synced: about 1 year ago - Pushed: over 2 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: about 1 year ago - Pushed: over 4 years ago - Stars: 5 - Forks: 2

andrewhao/tuxedo-tutes

🕴🏻 Introduction to TLA+ and formal verification methods

Language: TLA - Size: 87.9 KB - Last synced: about 1 month ago - Pushed: about 2 years ago - Stars: 0 - Forks: 0

johnyf/tlapy

Python utilities for working with TLA+ specifications

Language: Python - Size: 13.7 KB - Last synced: 9 days ago - Pushed: over 3 years ago - Stars: 0 - Forks: 0

josedusol/PCR

TLA+ specification of the PCR parallel programming pattern.

Language: TLA - Size: 804 KB - Last synced: about 1 year ago - Pushed: about 2 years ago - Stars: 1 - Forks: 1

polikow/bully_election

Bully election algorithm model written in TLA+ and PlusCal

Language: TLA - Size: 156 KB - Last synced: about 1 year ago - Pushed: over 2 years ago - Stars: 0 - Forks: 0

ashishnegi/learn_tlaplus

Learn TLA+ specification

Language: TLA - Size: 3.53 MB - Last synced: about 1 year ago - Pushed: almost 3 years ago - Stars: 0 - Forks: 0

Alexander-N/tlaplus-exercises

Jupyter notebook with exercises from https://learntla.com

Language: Jupyter Notebook - Size: 233 KB - Last synced: about 1 year ago - Pushed: about 3 years ago - Stars: 2 - Forks: 1

ArneVogel/tlaplus

Language: JavaScript - Size: 3.93 MB - Last synced: about 1 year ago - Pushed: almost 3 years ago - Stars: 0 - Forks: 0

dgpv/bip32_template_parse_tplaplus_spec

TLA+ specification of the parser for BIP32 path templates

Language: TLA - Size: 132 KB - Last synced: about 1 year ago - Pushed: about 3 years ago - Stars: 3 - Forks: 2

puchkovki/File-systems

Курс по Файловым системам для студентов 4-го курса ТИПИ ФПМИ, МФТИ

Language: C++ - Size: 1.04 MB - Last synced: 12 months ago - Pushed: over 3 years ago - Stars: 0 - Forks: 0

hengxin/formal-methods

Formal Methods

Size: 3.65 MB - Last synced: about 1 year ago - Pushed: over 3 years ago - Stars: 0 - Forks: 0