apalache

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

APALACHE: symbolic model checker for TLA+ and Quint

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

Material for a workshop on Apalache and TLA+. To be populated with more examples.

Rust library for consuming Apalache ITF traces

Protocol specs in Python you can verify: test, simulate, model check, prove

Hardening TLC and Apalache through systematic, differential, fuzz, and regression testing to improve the reliability of TLA+ model checking

Symbolic testing of TFTP with Apalache

Benchmarks for apalache

Examples of efficiently using Apalache

TLAki: Little cute typed definitions in TLA+

Python library to parse and emit Apalache/Quint traces as JSON ITF

Bug finding challenge for all of the tools around

Quint specification of Aztec governance and formal verification

Minimalistic Python client for interaction with the Apalache model checker over JSON RPC

Research-stage verification suite for a pure OCaml subset, BEAM actor protocols, and Idris2/Zig FFI boundaries. Targets Why3/SMT, Apalache, and checked proof receipts. Current contents are architecture, an implementation roadmap, and fail-closed readiness tooling; the proof engine is not yet implemented.

TLA+ Specification of Raft Consensus Algorithm

Interface files for the Apalache symbolic model checker reminiscent of OCaml

Web tool that turns TLA+ specs into actionable requirements, rewrites NFRs into TLA+ monitors, and runs proof checks via a backend.