The P programming language.

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

Advanced fuzzing via Model Based Testing for Cosmos blockchains

Please see https://github.com/hacspec/hax

A workbench for writing toy implementations of distributed systems.

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

Chai: Client for Human-Apalache Interaction

A 2-4h workshop on the Tamarin protocol verifier.

Protocols made fun: Igor's blog

A Clojure model checker (using the TLA+/TLC engine)

Rust library for consuming Apalache ITF traces

A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.

Creusot helps you prove your code is correct in an automated fashion.

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

Solarkraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache

TLAki: Little cute typed definitions in TLA+

Generate (message) sequence diagrams from TLA+ state traces

Examples of efficiently using Apalache

Formal specification of PBFT in TLA+

Tree Sitter grammar for Quint

A model-based testing framework for Quint + Rust

Agents and tools for using Quint with LLMs