Formal Specifications for AI Coding Agents, End to End

The bottleneck moved. Writing code became nearly free, and reviewing it did not, so teams merging dozens of agent-authored pull requests a week now find that acceptance, not generation, sets their shipping speed. Formal specifications for AI coding agents attack exactly that gap. Instead of re-deriving a 900-line diff, you audit a 50-line spec, and a model checker judges every implementation against it, including the ones your agent ships at 3 a.m.

This guide covers the whole loop: which code deserves a spec at all, a state-machine specification you can check in minutes, and the CI wiring that turns counterexample traces into merge gates the agent cannot talk its way past.

Why Agent Diff Volume Breaks Human Code Review

Review presumes a scarce diff. Run the arithmetic for an agent-heavy team. Thirty agent PRs a week at roughly 400 changed lines each is about 12,000 lines. A careful reviewer sustains perhaps 300 lines per hour, and that figure was calibrated on human-written code. Staying current would consume one engineer's entire week, every week, before touching any of the team's own work. So it does not happen. Approvals drift into acknowledgments, queues add days of latency, and review degrades into spot-checks precisely where agents are most productive.

Tests do not rescue this, for a structural reason. When the same agent writes the code and the tests, the suite encodes what the agent believed, not what the business requires, and nothing in the loop stops it from weakening an assertion to go green. These are the limits of AI-era code review at volume: reviewer attention is the scarce resource, and agent output scales without it. Acceptance criteria for AI-generated code need an artifact the agent satisfies only by actually conforming, one a human can audit faster than the diff can be read.

What Machine-Checkable Actually Means

Most teams already write specifications: tickets, ADRs, the markdown briefs that spec-driven development toolkits produce. The difference between spec-driven development and formal specification is who decides conformance. With prose, a human reads the implementation and judges, and an agent can satisfy the wording of a brief while changing behavior in ways the prose never anticipated. No tool objects, because no tool is reading.

Machine-checkable specifications sit on a four-rung ladder:

1. Prose. Tickets, briefs, spec-driven development markdown. Flexible, agent-editable, judgment required.
2. Typed schemas. OpenAPI, JSON Schema, database constraints. A tool verifies shape and presence, never behavior over time.
3. Executable specs. Specifications you can simulate, which kills ambiguity fast. Quint, a typed executable language, lives here and above.
4. Model-checked specs. TLA+ and Quint plus a checker that explores every state reachable within bounds you set and prints a counterexample trace when an invariant breaks.

The rung determines the trust property:

A markdown spec is a suggestion the agent can satisfy in letter while breaking in spirit. A model-checked spec is a contract the checker enforces on every reachable state.

Two caveats keep this honest. Bounded model checking yields strong evidence rather than proof, since exploration stops at the depth you configure. And a checker defends exactly the invariants you wrote, which is why spec authorship, discussed below, stays a human job.

Where Formal Specifications for AI Coding Agents Pay Off

Formal methods reward a specific shape of code: persistent state, transitions with preconditions, and invariants that must survive every interleaving. That is also where agent-written behavior carries the most risk, because the failure modes are invisible in any single diff.

Code pattern	Example	Proportionate acceptance layer
Money-bearing state machines	Order lifecycle: created, paid, shipped, refunded	Formal spec plus model checker
Concurrency and retries	Idempotency keys, double-spend races, oversell	Formal spec for invariants, property tests in code
Cross-service consistency	Ledger entries sum to balances	Formal spec plus reconciliation monitoring
Plain CRUD and glue	Endpoints mapping to a row	Types and contract tests
UI and exploratory code	Prototypes, internal tools	Review, flags, fast rollback

The payoff class is documented, not hypothetical. AWS engineers published a detailed account in Communications of the ACM (2015) of applying TLA+ to large real-world services, catching subtle bugs and forcing design fixes before code existed. The Azure Cosmos DB team has described using TLA+ in its internals as well. The pattern is current in the open, too: the Cosmos IBC protocol carries a production-grade Quint specification maintained by Informal Systems.

Triage ends with a simple test. If you cannot name an invariant worth defending, no refund before payment, an idempotency invariant where applying a payment twice moves money once, balances that never go negative, you do not have a spec-worthy module. Write tests and move on.

A Worked Order State Machine in Quint

Quint reads like typed pseudocode, and this order state machine example fits on one screen:

module order {
  type Status = Created | Paid | Shipped | Refunded | Cancelled

  const maxItems: int

  var status: Status
  var items: int
  var wasPaid: bool

  action init = all {
    status == Created,
    items == 0,
    wasPaid == false,
  }

  action addItem = all {
    status == Created,
    items < maxItems,
    items' == items + 1,
    wasPaid' == wasPaid,
    status' == status,
  }

  action pay = all {
    status == Created,
    items > 0,
    status' == Paid,
    wasPaid' == true,
    items' == items,
  }

  action ship = all {
    status == Paid,
    status' == Shipped,
    wasPaid' == wasPaid,
    items' == items,
  }

  action refund = all {
    status == Paid or status == Shipped,
    status' == Refunded,
    wasPaid' == wasPaid,
    items' == items,
  }

  action step = any { addItem, pay, ship, refund }

  invariant NoRefundBeforePayment = status == Refunded implies wasPaid
}

Run quint run order to simulate random executions, then quint verify order to model-check, keeping constants like maxItems small so the run finishes in seconds. The Quint documentation covers installation, simulation, and bounded checking.

The invariant looks redundant, since refund only fires from Paid or Shipped. That redundancy is the point. The checker proves the guard enforces the property across every reachable interleaving, so the invariant becomes a tripwire for future edits. Add one plausible-sounding transition, a goodwill refund from Created, rerun, and the checker prints a counterexample trace ending in a violated invariant. Example-based tests execute the paths someone imagined; the checker explores the ones nobody did, which is exactly where fluent, confident agents do their damage.

The same machine in TLA+ is nearly identical minus the type annotations, and Learn TLA+ state machines walks that version. On Quint versus TLA+ for beginners: Quint's types and instant feedback flatten the first week, while TLA+ carries the deeper literature. The transfer cost between them is a weekend, not a quarter, so pick one and start.

The Spec-First Agent Loop

The workflow, in order:

1. A human writes or audits the spec. States, transitions, invariants. Machine-drafted specs are drafts, and drafts get audited line by line.
2. Model-check the spec itself. Most of the value is design-stage; a counterexample here costs a conversation, not an incident.
3. The agent implements against the spec, which lives under path protection the agent cannot write.
4. Extract executable checks. Transition guards become assertions in the service; state machine invariants become checks after every state change, run as property tests.
5. Gate merges on the checker and the extracted checks, with counterexample traces routed back to the agent.

Step four is where spec-first development earns its name. The economics invert: scarce human attention goes to 50 lines of contract, cheap checker cycles go to every line of implementation, and a 900-line diff stops being the object anyone reviews by eye.

Wiring the Checker Into CI

Running a model checker in CI on agent diffs closes the loop mechanically. Four pieces:

• Protect the spec path. Branch rules plus CODEOWNERS so commits touching spec/ require human approval.
• Check the spec itself. A quint verify job on a spec this size finishes in seconds; TLA+ teams use TLC or Apalache.
• Map events to actions. An integration harness replays API calls and asserts guards and invariants after each step. An implementation event with no corresponding spec action fails the build: either the spec is missing behavior (a human fixes the spec) or the code grew behavior (the agent fixes the code).
• Feed traces back. A red build with a counterexample in the agent's context is a precise, checkable instruction: reproduce, fix, rerun. Agents close that loop quickly.

This wiring is what turns formal specifications for AI coding agents from a design exercise into an enforcement point. Verifying AI-generated code against a specification stops being a judgment call and becomes a computation CI runs on every diff.

What Agents Can and Cannot Do With Specs

The most underused capability is the one worth leading with: replaying recorded production traces against the executable spec. The full map runs three tiers, most established first.

Tier one, implementation. Agents build well against a fixed spec, because a checked spec is the clearest prompt you will ever hand one. Every guard and invariant is unambiguous in a way prose never manages.

Tier two, repair. Agents convert counterexample traces into fixes quickly. A trace names the exact states that led to the violation, so the work is mechanical rather than investigative.

Tier three, replaying reality. This is trace validation, or model-based testing with recorded data: capture what production actually did, as sequences of operations and state changes, then check each sequence against the spec's guards and invariants. It answers the weakness flagged earlier in this guide, where a suite the agent wrote itself "encodes what the agent believed, not what the business requires." Recorded traces are the antidote, because they encode what the business requires: they are what reality did, not what anyone, human or agent, imagined. The scenarios include the odd interleavings nobody would script on purpose. None of this needs new machinery, either, since Quint's executability, the property that let the worked example simulate random runs, is exactly what makes replaying a real trace possible. A spec you cannot execute is a spec you cannot replay.

Authorship remains the honest limit. Reported experiments with LLM-written TLA+ suggest models can draft specs that pass shallow checks while missing the edge cases and liveness conditions the spec existed to catch. A machine-drafted order spec that quietly omits the double-refund case still checks green; a missing "every order eventually settles" condition never fails a safety check at all. The division of labor holds for now: agents write implementations and first drafts, humans own the spec, or audit a machine draft line by line with the care they would give their own writing.

When Formal Specs Are Overkill

The honest case against formal specifications for AI coding agents is proportionality. The costs are real: days to weeks of learning, maintenance whenever behavior changes, checker time that grows with the state space. And most code lacks the paying shape entirely. UI, glue, one-off scripts, and prototypes hold no persistent state machine and no invariant anyone would escalate at 2 a.m. For those, the ladder stops earlier. Strict types catch shape errors cheaply. Property-based testing, in the Hypothesis style, generates adversarial inputs and shrinks failures to a minimal readable example. Invariant monitoring and reconciliation catch what escaped to production. Knowing when formal methods are overkill is part of the skill; a team that formally specifies its internal to-do app has learned the notation and missed the point.

A 30-Day Starting Path

Scope it to one stateful service, not the codebase.

Week 1. Choose the service, whether orders, subscriptions, or a wallet. List states and transitions on one page. Name two invariants.

Week 2. Write the Quint spec, around 50 lines. Simulate, then verify, with small bounds so runs finish in seconds.

Week 3. Have the agent implement or refactor against the spec. Map implementation events to spec actions. Lift invariants into property tests.

Week 4. Turn on the CI gate and spec-path protection. Route counterexamples to the agent automatically.

Success signals after a month: human review time per agent PR drops, at least one invariant violation is caught before merge (a single catch usually pays for the month), and the spec still fits under roughly 100 lines. If it balloons, you specified two machines. Split them.

The Underlying Trade

The bottleneck moved, and the trade underneath every workflow in this guide is that human judgment is scarce and checker cycles are not. Spend the scarce thing once, on a contract a person writes and audits, and let the cheap thing enforce it on every diff. Agents scaled the writing; formal specifications are how the checking keeps up.