Pimp My IDE / Garage dispatch
Back to garage
September 27, 2026 | formal methods / agents / distributed systems

A generated spec is not a safety certificate.

TLA+ can expose a bad system design before the code exists. The useful output is the invariant and the counterexample, not a ceremonial file beside the repository.

The take. Bound the model, run the checker, save the failing trace, and replay the same condition against the implementation. Keep each claim attached to the layer that earned it.
Route the counterexampleRead the field guide

The model checks the model.

TLA+ describes system states, allowed transitions, and properties over possible executions. TLC explores reachable states for a finite instance and reports a trace when the model violates a checked property.[1] That is stronger than asking an agent whether a design looks safe. It is narrower than proving the running software behaves the same way.

The new Reasonable guide makes that boundary explicit. Its leader-election example has 38 states for three computers and more than one million for nine. The guide also warns that a TLA+ specification is usually separate from the implementation. The two can drift.[1]

A counterexample is a route through your model. The next job is to make the implementation drive that route.

Ask safety and liveness separately.

A safety property says that a bad condition never occurs. In leader election, two leaders at once would violate safety. A liveness property says that a desired condition eventually occurs. A system that never elects anyone can satisfy the safety rule while remaining useless.[1]

This split matters when an agent drafts the specification. A clean safety result may hide a dead system. A liveness claim may depend on fairness assumptions that the implementation, scheduler, or network does not honor. Put the property and every assumption in the review packet.

Use the spec as a map, not a trophy.

Datadog describes TLA+ specifications as one layer in a larger verification stack. Its published workflow also uses deterministic simulation, bounded verification, model checking, compatibility tests, and staging telemetry. The article calls deterministic simulation the main workhorse and TLA+ the map that defines state variables, actions, and invariants.[3]

Those performance and production results are Datadog's reports about its own systems. They do not prove that an agent-generated spec matches another codebase. The reusable idea is the transfer path. Reuse the same invariant across the model, test harness, and live checks. When the checker returns a trace, turn it into an implementation test.

Make the handoff executable.

Leslie Lamport describes TLA+ as a language for modeling concurrent and distributed systems. His site distinguishes the TLC model checker from the TLAPS proof system.[2] The TLA+ Wiki calls TLC an explicit-state checker for a commonly used subset of TLA+, especially finite systems. It can also dump a violation trace as JSON.[4]

A practical counterexample packet needs these parts:

  1. The specification revision and model configuration.
  2. The exact property, assumptions, constants, and finite bounds.
  3. The checker command, version, result, and failing trace.
  4. An implementation test or deterministic simulation that recreates the trace.
  5. A result from the code revision that will ship.

If the bridge to code is missing, say "model checked." Do not say "implementation verified." Precise language is part of the control system.

Interactive makeover / verification handoff

Counterexample transfer case

Traditional purpose replaced: a checkbox that says "formal methods done." Better version: route one claim through an ordered evidence trace, choose the required packet sections, and print every field that still needs real output.

Choose the packet focus

The focus changes the handoff wording. It does not increase the evidence.

Review focus
Packet sections
Specification focus1 of 4 sections selected
01
Write the transition modelDefine states, allowed actions, properties, and assumptions before asking the checker for a result.
Packet focusSpecification fields
Next missing sectionProperty fields

Specification focus. Stage 1 of 5. 1 of 4 packet sections is selected.

Print the trace packet

All four sections complete the packet structure. Real checker output and a code replay are still required.

Sources read, not vibes

Open the source log
  1. Reasonable, "The internet discovers TLA+. Now what?", published September 25, 2026 and read September 27, 2026. This is the source for the transition-system explanation, safety and liveness examples, 38-state and million-state figures, and spec-to-implementation caveat.
  2. Leslie Lamport, "My TLA+ Home Page", last modified October 13, 2025 and read September 27, 2026. This identifies TLA+'s purpose and distinguishes the TLC model checker from the TLAPS proof system.
  3. Datadog, "Closing the verification loop: Observability-driven harnesses for building with agents", published March 9, 2026 and read September 27, 2026. This is the source for Datadog's verification stack, reported project results, and its description of TLA+ as a map within a larger harness.
  4. TLA+ Wiki, "TLC Model Checker", read September 27, 2026. This documents TLC as an explicit-state model checker, its finite-system focus, and JSON trace output.
  5. Hacker News discussion 49863600, verified through the official item API and page on September 27, 2026. It is the discovery route. The discussion does not verify the article's technical claims.

Source boundary. Reasonable explains the method and presents its own interactive example. Lamport and the TLA+ Wiki document the language and checker. Datadog reports its own engineering workflow and outcomes. The transfer case is a planning control. It does not execute a model checker or inspect code.