TLA+ projects, tools, and research

Modeling, model checking, and LLM-assisted specification work.

TLA+ Generator · tlakit · AI4FM · research

I use TLA+ to model systems small enough to inspect and large enough to hide mistakes. TLA+ is a language for describing state machines and checking properties over their reachable states. The projects include small models of laptops, walk-in ovens, a Dexcom G7 session, microwaves, and game mechanics.

The research side studies whether language models can produce specifications that survive execution by SANY and TLC rather than merely matching an expected string. The related repositories include the ChatTLA+ corpus and benchmark, TLA-Prove, TLA-Extraction notes, the TLA+ dataset pipeline, and tlakit, a Python and notebook client for the TLA+ toolchain.

TLA+ Generator is the browser-facing entry point. It accepts a natural-language description, generates a specification, and runs a correction loop until the available syntax and model checks pass. The publication summaries connect the papers with their training code, models, and datasets.

Scope

The examples are models and research tools, not certified controllers. A passing TLC run covers the states and properties encoded in the model; it does not establish that the model represents every behavior of the real system.