Access large language models from the command-line

Curated list of resources on testing distributed systems

Semi-automated modelling and Model-Based Testing for CosmWasm contracts

Go library for un/marshalling ITF files

QA infrastructure for CometBFT

Rust library for consuming Apalache ITF traces

CometBFT: A distributed, Byzantine fault-tolerant, deterministic state machine replication engine. A fork and successor to Tendermint Core.

Model-based testing tool

VS Code extension for viewing ITF traces

Advanced fuzzing via Model Based Testing for Cosmos blockchains

TLA+ language support for Visual Studio Code

Utilities for the TLA+ ecoystem and model-based testing using TLA+.

The Z3 Theorem Prover

Dafny is a verification-aware programming language

BFT-SMaRt's project home page

Sawtooth PBFT consensus engine

Verification framework and tool for higher-order Scala programs

Solver for higher-order functional programs, used by Stainless

Pedagogical first-order prover in Python

Python interpreter for TLA+ specifications

A collection of simple message transformers for Kafka Connect

Learn how to design large-scale systems. Prep for the system design interview. Includes Anki flashcards.

APALACHE: symbolic model checker for TLA+ and Quint

Free and Open Source, Distributed, RESTful Search Engine

Embeddable multi-Paxos For The JVM

Cog - A Free and Open Source Audio Player for macOS 10.13+

Google core libraries for Java

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

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