Verification tool for distributed protocols based on inductive proof decomposition.

For when people get too hyped up about things

The TLA⁺ Proof Manager

A thin thread-safe wrapper around Python's sqlite3

A demonstration of the Checker Framework and Lombok working in harmony

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

Learn TLA+ for free! No prior experience necessary!

Dependency validator detects runtime compatibility issues at build time

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

Pluggable type-checking for Java

A model checker for implementing distributed systems.

Proving leftpad correct two-dozen different ways

Lossless codec for numerical data

egg is a flexible, high-performance e-graph library

Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs

Example multi-paxos application for those learning Paxos & multi-paxos

Specifications and safety proofs in different tools of a simple concurrent algorithm

What are the differences between the transaction isolation levels in databases? This is a suite of test cases which differentiate isolation levels.

APALACHE: symbolic model checker for TLA+ and Quint

This cleans up duplicate SMS entries in a backup created by SMS Backup & Restore Android app.

A LaTeX package for proof carrying papers

Guide to Python's magic methods

A demo implementation of a simple dependently-typed language

TattieBogle Xbox 360 Driver (with improvements)

Unit-Test Based Programming

An Operating Function

A block device in user space for Linux

Rainbows and unicorns!