pluscal
There are 24 repositories under pluscal topic.
tlaplus/Examples
A collection of TLA⁺ specifications of varying complexities
tlaplus/DrTLAPlus
Dr. TLA+ series - learn an algorithm and protocol, study a specification
tlaplus/vscode-tlaplus
TLA+ language support for Visual Studio Code
tlaplus/CommunityModules
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
DistCompiler/pgo
PGo is a source to source compiler from Modular PlusCal specs into Go programs.
fizzbee-io/fizzbee
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
tlaplus-community/tree-sitter-tlaplus
A tree-sitter grammar for TLA⁺ and PlusCal
mrc/tla-tools
TLA+ tools for Emacs
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).
VadimPlh/Arrival
How to use TLA+ / TLA+ specification of the ClickHouse replication protocol
rberenguel/tla_lightning
Lightning talk about TLA+ for Scala Exchange 2018
sanjosh/tlaplus
TLA+ programs
hengxin/tlaplus-pluscal-utils
Utilities for TLA+ and PlusCal
hvanz/PaxosInPluscal
Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.
jb567/tla-go-back-n
A TLA+ verification of the Go-Back-N ARQ protocol
Gulfam92/DistributedSystems-Algorithms-ModelChecking
Implementation and validation of the model checking of various Distributed System algorithms like BenOr, Paxos, etc. using PlusCal and TLA+, also analyze the temporal and invariant properties.
melintea/upml
Formal verification of UML state machines with Promela and TLA+/PlusCal
orsinium-labs/simple-tla
Collection of useful "operators" (functions) to make TLA+ easier to learn and to use
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.
BoeVonLipwig/Go-Back-N-TLA-
Go-Back-N specified in TLA+/ PlusCal
polikow/bully_election
Bully election algorithm model written in TLA+ and PlusCal
flakas/tla-experiments
Experimenting with formal methods using TLA+ and Pluscal
skhoroshavin/tla_playground
Learning and experimenting with TLA toy models