pluscal

A collection of TLA⁺ specifications of varying complexities.

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

TLA+ language support for Visual Studio Code

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

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

PGo is a source to source compiler from Modular PlusCal specs into Go programs.

A tree-sitter grammar for TLA⁺ and PlusCal

TLA+ tools for Emacs

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).

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

Lightning talk about TLA+ for Scala Exchange 2018

TLA+ programs

Erla+ is a compiler that transpiles PlusCal specs into Erlang implementations

Repository for my master's thesis containing translation tool, erlang code, generated gen-server

Formal verification of UML state machines with Promela/spin and TLA+/PlusCal

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

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

A beautiful, dark-mode cheat sheet for PlusCal.

Utilities for TLA+ and PlusCal

When a process is betrayed and sent into a limbo by a fellow process, it regains its majority and comes back for consensus.