Tutorial on modeling with TLA+

Tool qualification tests and reports for the TLA+ model checker

Some experiments in making exercises for teaching TLA+

A formatter for TLA+ specs

TLA+ and Distributed/Discrete Systems.

TLA+ Foundation

Verification tool for distributed protocols based on inductive proof decomposition.

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

A formatter for the TLA+ language.

Eco CI Energy estimation for Github Actions Runner VMs

A user-ready linux image/rootfs for the Pine64 Pinenote based on Debian trixie and GNOME

TLA+ Unicode input for Emacs

APALACHE: symbolic model checker for TLA+ and Quint

In Spec We Trust

Add hardship to your tests

Hermit launches linux x86_64 programs in a special, hermetically isolated sandbox to control their execution. Hermit translates normal, nondeterministic behavior, into deterministic, repeatable beh…

A collection of TLA⁺ specifications of varying complexities.

Tool for automatically inferring inductive invariants of distributed protocols.

Replicated State Library. RSL is the Azure Paxos implementation which is used by multiple products in Azure and Bing. It provides the traditional Paxos functionality in a real world implementation.…

Artifact package accompanying our POPL 2024 submission titled "A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability".

A finite model checker for exhaustively testing C# code

A framework for distributed applications

Code for use in Wikipedia articles

Q# code snippets written when exploring quantum computing concepts

TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

Exploring concepts & tools in computerized mathematics

For testing tree-sitter grammar functionality

Personal website for outdoor trip reports

Incomplete tree-sitter grammar for the PRISM probabilistic modeling language