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

A ground-up Rust rewrite of the TLA+ tools (SANY + TLC, safety subset), compiled to a 509 KB WebAssembly module and served from Cloudflare's edge. No JVM. No install. An MCP server your coding agent can call natively.

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

509 KBwhole 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. If a property can be violated, you get the shortest counterexample trace — the exact step-by-step scenario that breaks your design. If the state space explodes, you get a per-level growth profile and a hint about which constant to shrink, instead of a hung process.

Use it from Claude (MCP)

The service speaks the Model Context Protocol at /mcp (Streamable HTTP, stateless). One command registers it in Claude Code:

claude mcp add --scope user --transport http tlc \
  https://tlc.proc.io/mcp \
  --header "Authorization: Bearer $TLC_API_TOKEN"

Two tools appear: tlc_check (full model check — pass the module source and TLC config, get state counts, traces, diagnostics) and tlc_parse (fast syntax + semantic + level check). Your agent keeps the spec next to the code, updates it when the architecture changes, and verifies every change in seconds — a formal-methods reviewer on tap.

Use it from anything else (REST)

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

Response is JSON: 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.

Why this is cool

Model checkers have always meant "install a JVM, download a jar, babysit a process." This one is a stateless function at the edge: the entire checker — 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 — boots in microseconds inside a V8 isolate near you.

Correctness isn't asserted, it's measured: every build is differentially tested against the reference Java implementation on a mined conformance suite, matching its verdicts, exact state counts, and counterexample depths. Where the two disagree, the discrepancy is documented and traced to an upstream bug, not shrugged off.

And because it's MCP, the checker composes with agents: "keep the spec in sync with the architecture and prove my invariants still hold" becomes a background loop, not a chore.

Scope