`tlc.proc.io`: hosted TLA+ model checking

The TLA+ tools (SANY + TLC, safety subset) rewritten in Rust, compiled to a 509 KB WebAssembly module, and served from Cloudflare's edge. Onboarding consists of a free passkey account and an API key, and any HTTP client can use the service. Point a coding agent at it and formal verification becomes a routine part of development. Source on GitHub.

97/107exact-parity conformance vs Java TLC (verdict, state counts, trace length)

509 KBthe whole checker as wasm: parser, level checker, evaluator, BFS engine

≤30 sself-limiting runs with a state-blowup diagnostic on timeout

What it does

You write a TLA+ specification of your system and a small config. The service exhaustively explores every reachable state, checking your invariants and [][A]_v action properties on each transition. When a property can be violated, you get the shortest counterexample trace (the exact step-by-step scenario that breaks your design). When the state space grows too large, you get a per-level growth profile and a hint about which constant to shrink.

Start in one command (MCP)

The service speaks the Model Context Protocol at /mcp. Sign in with a passkey at /account (the only identifier the service holds is a random UUID), mint an API key, and register the endpoint in Claude Code; the tools appear: tlc_check, tlc_parse, and tlc_report_win:

claude mcp add --scope user --transport http tlc https://tlc.proc.io/mcp \
  --header "Authorization: Bearer <your key>"

That completes the setup. Ask your agent to model-check something and it will call tlc_check with the spec source and TLC config directly.

Publish to the hub

Every passing tlc_check publishes its spec and config to the hub automatically: your agent iterates on a design, and the hub keeps one generation per revision of each module, forming a public, growing library of specs that are known to pass the checker. Publishing is on by default; turn it off account-wide on /account or per call with publish: false. Unpublished runs are processed in memory and discarded when the request completes.

When a counterexample trace exposes a genuine design bug, and the corrected design then passes, your agent records the save with tlc_report_win. Wins appear on the spec's hub page and in the site-wide wins list: a public record of bugs formal methods caught before they shipped.

Recommended practice

The high-leverage pattern is a standing instruction in your project's CLAUDE.md (or equivalent) so the spec evolves with the code:

In a separate agent, keep specs/ up to date using TLA+ as you
go. Update the .tla file whenever the architecture changes, then
validate with the tlc_check MCP tool. Run this in the background
so the main work keeps moving. When a check passes, save the
exact .tla and .cfg you used into specs/ so the passing
configuration lives with the code. Keep specs finite: small
CONSTANT sets, bounded ranges. On invariant_violation, read the
trace and fix the design or the spec. When the trace exposed a
real design bug and the corrected design passes, report the win
with the tlc_report_win MCP tool. On timeout, read the
diagnostic hint and shrink constants.

Spec-writing tips that keep checks fast and meaningful:

Model sets of 1–3	Two users and one resource usually expose the same interleavings as ten, at a fraction of the states.
Strings as statuses	Enumerated string states (`"pending"`, `"active"`) keep specs readable and compare fast.
TypeOK first	A type invariant catches most modeling mistakes immediately and documents your state shape.
Action properties	`[][A]_vars` properties (say, "closed records stay closed") check per-transition claims that invariants can't express.
CHECK_DEADLOCK FALSE	Set it when terminal states are intentional, so quiescence reads as success.

REST, for everything else

The same API key authenticates the raw endpoints:

curl -s https://tlc.proc.io/check \
  -H "Authorization: Bearer <your key>" \
  -H "Content-Type: application/json" \
  -d '{"modules":[{"name":"Spec","source":"---- MODULE Spec ----\n..."}],
       "config":"INIT Init\nNEXT Next\nINVARIANT TypeOK",
       "timeoutSeconds":30}'

The response carries status (ok, invariant_violation, deadlock, timeout, …), stats, a violation.trace when something breaks, and a diagnostic with per-level state growth when the space blows up. POST /parse runs the fast syntax and level check alone.

Why this is interesting

Model checking has traditionally required a local toolchain: a JVM, the tla2tools.jar distribution, and a long-running process to supervise. This implementation is a stateless function at the edge: a hand-written parser faithful to SANY's column-sensitive junction-list grammar, a value system whose 64-bit fingerprints are bit-identical to Java TLC's, and a breadth-first search engine, all booting in microseconds inside a V8 isolate near you.

Correctness is measured continuously: every build is differentially tested against the reference Java implementation on a mined conformance suite, matching its verdicts, exact state counts, and counterexample depths. Because the checker is one MCP tool call away, "prove my invariants still hold" becomes part of an agent's inner loop, on every architecture change, in the background.

What is implemented, what is omitted, and why

This engine implements the safety subset of TLA+: the full expression language, invariants, deadlock detection, box-action properties ([][A]_v), CONSTANT assignments with model values, CONSTRAINT/ACTION_CONSTRAINT, and EXTENDS-based modules (Naturals, Integers, Sequences, FiniteSets, TLC, and Bags are built in). That subset was chosen deliberately: it covers what agent-written specs of real systems actually use (state machines, type invariants, "closed things stay closed" claims), and every feature in it is verified against Java TLC exactly.

Omitted features, and the reasoning behind each omission:

Liveness & fairness	Checking `<>P` or `WF_v(A)` requires a tableau construction and cycle detection over the full behavior graph, a second engine roughly the size of this one. Safety questions ("can this bad thing ever happen?") are where agent workflows get their value.
Parameterized INSTANCE	Module instantiation with substitutions (`I == INSTANCE M WITH x <- y`, `I!op`) brings in SANY's largest single subsystem. Plain `EXTENDS` composition covers the common case; this is the most likely next addition.
ENABLED	Deciding whether an action could fire requires a nested successor search inside expression evaluation. Contained, and on the shortlist.
Symmetry sets	A performance optimization (quotienting the state space by permutations), and one that changes reported state counts. Small finite models rarely need it.
Proof syntax	`THEOREM ... PROOF` and ASSUME/PROVE belong to TLAPS, the proof system. A model checker only needs the propositions.
Reals, RandomElement	Real arithmetic is unenumerable, and randomized operators give different answers run to run, which conflicts with this project's exact-parity standard.

The 97/107 conformance figure reads accordingly: 97 cases match Java TLC exactly, zero cases mismatch, and the remaining 10 exercise the features above. The engine recognizes them and returns a clean unsupported_feature status (with the local tla2tools.jar as the documented fallback) rather than a wrong answer. Keep specs finite (small constant sets, bounded ranges) and the supported subset is a complete, trustworthy checker.

tlc.proc.io: hosted TLA+ model checking