Stackness
All moves

Writing TLA+ specifications alongside agentic implementation

by Stackness

Languages & Frameworks

Teams are pairing formal specification languages like TLA+ with coding agents: model the intended system behaviour as a temporal specification first, then have the agent implement against it and eventually generate machine-checked proofs. The goal is a loop where software is specified, implemented and verified together instead of a spec written once and never checked again. Related efforts formalize existing bodies of knowledge in proof assistants like Lean as part of the same push toward machine-checked correctness.

What it is

This move treats a formal specification, written in a language like TLA+, as a first-class artifact that sits next to the code an agent produces, rather than a document written once and forgotten. TLA+ lets you describe a system as states and the actions that move it between states, plus temporal properties such as safety conditions that must always hold or liveness conditions that must eventually hold. A model checker then explores reachable states of that model and checks whether the properties survive. The specification does not verify the real implementation by itself, since it only checks a finite model of the software, but it gives a precise target for an agent to build against and for humans to review.

How to do it

  • Pick a component with real coordination or concurrency risk, such as leader election, a consensus step, or a state machine with tricky edge cases.
  • Write the TLA+ model first: define the states, the actions that transition between them, and the properties you actually care about, for example that no two leaders exist at once.
  • Run the model checker to find counterexamples before any implementation code exists, since short traces can hide bugs that only surface after many steps.
  • Hand the specification to a coding agent as the contract for the implementation, and have the agent implement against it.
  • Where possible, push toward machine-checked proofs linking specification, proof and implementation, using proof systems that let specification and code share a language, or by generating proofs from specification and property pairs at scale.
  • Treat the loop as ongoing: specify, implement, verify, and revisit the spec as behavior changes.

When it helps

This pays off most for distributed or concurrent systems where bugs can require dozens of steps to trigger and are easy to miss in design review, code review, and conventional testing alike. It is also useful when you want an agent's output checked against an explicit, unambiguous description of intended behavior instead of prose requirements.

Pitfalls

A passing model checker only tells you the model satisfies the properties, not that the code does, and the checker typically explores only finite instances. Formal methods practice is uncommon, so both writing sound specifications and reviewing agent-generated ones takes real skill. Related efforts formalizing existing knowledge in proof assistants show the same tooling is still maturing, and full specification-to-proof-to-implementation loops are only starting to become tractable at scale.

Sources