tlaplus

Star

Here are 51 public repositories matching this topic...

tlaplus / Examples

Star

A collection of TLA+ specifications of varying complexities

algorithm protocol pluscal tlaplus

Updated Aug 18, 2020
TLA

tlaplus / DrTLAPlus

Star

Dr. TLA+ series

algorithm protocol pluscal tlaplus

Updated Jan 28, 2020
TLA

lemmy / BlockingQueue

Star

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!

java specification model-checking fifo fifo-queue tlaplus tlaps

Updated Aug 12, 2020
TLA

ligurio / practical-fm

Star

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

coq software-engineering formal-methods formal-verification tlaplus tla-specification

Updated Jul 28, 2020

informalsystems / apalache

Star

APALACHE: symbolic model checker for TLA+

model-checking smt tla tlaplus

Updated Aug 25, 2020
Scala

tlaplus / CommunityModules

Star

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

pluscal tlaplus tla-specification

Updated Aug 20, 2020
TLA

hwayne / tlacli

Star

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

formal-methods tlc tlaplus

Updated Feb 17, 2020
Python

will62794 / tlaplus_animation

Star

A TLA+ module for animating TLC traces.

tlaplus

Updated Feb 17, 2020
TLA

lorin / tla-linearizability

Star

Reading the linearizability paper with TLA+

linearizability tlaplus

Updated Nov 8, 2018
TLA

mryndzionek / tlaplus_specs

Star

Different TLA+ specifications, mostly for learning purposes

graphviz model-checking tla tlaplus tla-specifications

Updated Feb 23, 2020
TLA

pascalpoizat / fbpmn

Star

🔬 formal tools for BPMN

research bpmn verification tlaplus

Updated Jul 19, 2020
Haskell

mrc / tla-tools

Star

TLA+ tools for Emacs

emacs emacs-mode tla pluscal tlaplus

Updated Aug 15, 2020
Emacs Lisp

talex5 / spec-vchan

Star

A TLA+ specification for the Xen vchan protocol

xen specification tlaplus

Updated Jan 11, 2019
TLA

decanus / rutschblock

Star

A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+

tla formal-specification tlaplus tla-specification

Updated May 8, 2020
TLA

statechannels / tla-specs

Star

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

ethereum blockchain state-channels formal-models tlaplus

Updated Jun 12, 2020
TLA

dgpv / SASwap_TLAplus_spec

Star

TLA+ specification for Succinct Atomic Swap smart contract

bitcoin smart-contracts tla atomic-swap tlaplus tla-specification

Updated Jul 3, 2020
TLA

will62794 / snapshot-isolation-spec

Star

A formal specification of snapshot isolation in TLA+.

formal-methods tlaplus

Updated Jul 18, 2019
TLA

VadimPlh / Arrival

Star

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

distributed-systems clickhouse tla pluscal tlaplus

Updated Jun 18, 2019
TLA

JYwellin / CRDT-TLA

Star

Specifying and Verifying CRDT Protocols using TLA+

tlc tlaplus crdt-tla

Updated Oct 23, 2019
TeX

Disalg-ICS-NJU / tlaplus-lamport-projects

Star

Learning [Lamport's TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).

theorem-proving model-checking tlc tla-hyperbook lamport-specifying-systems tlaplus-video-course tlaplus tlaps

Updated Jul 16, 2019
TeX

vacp2p / formalities

Star

Formal models of vac protocols

formal-methods tla formal-specification tlaplus

Updated Mar 18, 2020
TLA

changlinli / peterson-tlaplus

Star

A TLA+ Specification of Peterson's Algorithm

concurrency tla-plus tlaplus

Updated Sep 27, 2019
TLA

mssabr01 / ICSVerifiedSoftwareProject

Star

A formally verified implementation of a bolt-on security device for ICS networks. Designed with TLA+ and written/proved in F*

security proof verification formal-methods fstar ics-security sel4 tlaplus

Updated Jan 11, 2020
C

dgpv / bip32_template_parse_tplaplus_spec

Star

TLA+ specification of the parser for BIP32 path templates

bitcoin tla bip32 tlaplus tla-specification

Updated Jul 20, 2020
TLA

visualzhou / tla-trace-formatter

Star

Parse the trace of TLC output and generate HTML with better format.

tla tlaplus

Updated Nov 7, 2019
Python

hvanz / PaxosInPluscal

Star

Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.

distributed-systems verification paxos formal-verification tla formal-specification formal-proofs pluscal tlaplus

Updated Sep 19, 2018
TLA

informalsystems / apalache-tests

Star

Benchmarks for apalache

tests tlaplus apalache

Updated Aug 27, 2020
SMT

hengxin / tla2tex

Star

TLA+ Code to TeX Code using tla2tools.jar

tex tla tlaplus tla2tex

Updated Aug 10, 2020
TeX

dgpv / ABL_contract_TLAplus_spec

Star

TLA+ Specification for Asset-Based Lending smart contract state transition table generation

smart-contracts tlaplus

Updated Aug 27, 2020
TLA

hengxin / cure-kvstore-tla

Star

TLA+ Spec for the Cure Key-Value Store

cure key-value-store causal-consistency tlaplus

Updated Feb 11, 2020
TeX

Improve this page

Add a description, image, and links to the tlaplus 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 tlaplus topic, visit your repo's landing page and select "manage topics."

Learn more