Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

Jupyter kernel for TLA⁺

Python interpreter for TLA+ specifications

Model-based testing tool

A simple REPL for TLA+.

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

Temporal Logic of Actions Modeling for Python

Parse the trace of TLC output and generate HTML with better format.

Measuring the growth of open source formal methods

Bazel rules for TLA+.

Python utilities for working with TLA+ specifications

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

Parser and syntax tree for TLA+, the temporal logic of actions

Self-supervising TLA+ formal verification loop — an LLM agent iteratively writes specs and fixes bugs, using the TLC model checker as an incorruptible evaluator. Inspired by Karpathy's autoresearch.