Formal Specs Are Incident Tools, Not Academic Proofs

There is a moment in every real incident where the room stops talking about features and starts talking about time.

Time to stop the bleeding. Time to understand what state the system is in. Time to decide whether a restart makes things better or makes the blast radius bigger. Time to answer the one question your future self will hate you for ignoring: “If we do nothing, what happens next?”

In that moment, most distributed systems turn into a story-telling contest. Everyone has a plausible narrative. None of the narratives are falsifiable fast enough.

This is why I keep coming back to formal specifications. Not as a purity test. As an incident tool.

Hillel Wayne put it plainly in his recent conversation on formal methods: formal methods are not only about proving programs correct, they are about making the critical parts of systems precise enough to reason about. That precision is the difference between “we think” and “we know,” especially when the system is distributed, automated, and under load.

The real problem is not bugs. It is state you cannot explain.

Most teams already know how to fix a bug. You find the repro, you patch, you ship. The hard problems show up when the system has multiple writers, asynchronous work, retries, partial failures, and timeouts that interact.

Now add agents.

An agentic workflow is not just code that runs. It is code that decides, then takes actions that create more state. If it calls external services, if it triggers payments, if it places orders, if it updates customer entitlements, every action becomes part of a chain you may have to justify later.

When this goes wrong, the failure mode is rarely “it crashed.” The failure mode is “it continued, but in the wrong reality.”

• Two workers both think they own the same job.
• A retry turns a once-only action into an at-least-once action.
• A human sees a dashboard that is eventually consistent and makes a decision based on a ghost state.
• An agent reads stale context and confidently performs a valid action at the wrong time.

Traditional testing does not cover this well because you cannot enumerate the interleavings that matter. Observability helps you see what happened, but only after the fact. “We have logs” is not the same as “we have a model.”

Formal specs, especially TLA+, force you to define the system as a state machine: what state exists, what transitions are allowed, what must always be true. That is not academic. That is the only way I know to make distributed behavior legible.

Determinism is not an implementation detail. It is a business requirement.

In trading and payments-adjacent systems, the goal is not “no incidents.” The goal is “bounded damage, explainable outcomes, and fast recovery.” You can live with a component failing. You cannot live with not knowing what it did.

Determinism, in practice, means four things:

1. Idempotence is explicit: you decide which actions can be repeated safely, and you encode the key that makes them safe.
2. Ordering is intentional: you choose where order matters (per account, per portfolio, per customer), and where it does not.
3. Ownership is singular: one place decides, others observe. If multiple places decide, you model arbitration.
4. Invariants are non-negotiable: you define what must never happen, even during retries, backfills, or partial outages.

This is the same mental shift that makes AI systems safer. Not because AI is magic, but because it is probabilistic. If you let probabilistic components write directly into your financial truth or your system of record, you lose the ability to replay and defend outcomes. Put them in the narrative layer, and keep the truth layer deterministic. (That separation is a cousin of what I argued in LLMs Belong in the Narrative Layer, Not in the Financial Truth Layer.)

Formal specs sit right at that boundary. They are a way to pin down the deterministic core and its invariants, so the rest of the system can be creative without being dangerous.

What TLA+ buys you under incident pressure

The most underrated value of TLA+ is not the model checker. It is the conversation it forces.

When you write a spec, ambiguity has nowhere to hide. You cannot say “the worker picks up the job.” You must define when it is eligible, who can claim it, and what happens if two workers try. You cannot say “we reconcile later.” You must define the reconciliation transition and what it is allowed to change.

Under incident pressure, that precision pays in three concrete ways:

• Auditability: you can map observed events back to allowed transitions. If something happened that is not in the model, you have a real defect, not a mystery.
• Recoverability: you can design the “repair moves” up front. Backfill, replay, compensation, and freeze paths are transitions too. If you never modeled them, you will improvise them when it is most expensive.
• Blast radius control: invariants tell you what you can safely relax and what you must protect at all costs. That clarity beats heroics.

This aligns with Wayne’s emphasis that formal methods are increasingly practical, and that tools like TLA+ are used because they help teams reason about complex behavior, not because they deliver perfect software. That pragmatic framing is the one that matters in a business setting. You are not buying certainty. You are buying fewer unknown unknowns. (Again, see the discussion.)

A lived pattern: the incident where “we can’t tell” is the real outage

I have built trading automation where the code was not the scary part. The scary part was the invisible contract between components: who is allowed to act, under what preconditions, and how we know an action is final.

One class of incident kept repeating across systems and teams: the system did what it was “allowed” to do locally, but globally it violated intent. A retry fired after a timeout, an acknowledgement arrived late, two services disagreed on whether a state transition had committed. The outage was not downtime. The outage was uncertainty.

When you cannot tell whether a state transition happened, you cannot safely proceed. You freeze. Humans start running manual scripts. People propose restarting queues and redeploying services because those are the only levers they can see. Meanwhile, the system continues to drift.

A formal spec would not have prevented every failure. But it would have made two things unmissable:

• The exact invariants that define “correct enough” behavior.
• The exact transitions that are safe recovery moves, including which ones are forbidden.

That is what I mean when I say it is an incident tool. It is a way to reduce the surface area of improvisation.

How to adopt formal specs without turning it into theater

You do not need a company-wide formal verification program. You need one narrow place where ambiguity is expensive.

Here is a pattern that works in real teams:

1) Pick one “truth workflow” and draw the boundary

Choose a workflow where wrong state is worse than downtime. Examples: entitlements, billing state, order lifecycle, portfolio positions, payouts, irreversible side effects.

Define what is inside the deterministic core (state machine, invariants, transitions), and what is outside (UI, analytics, agent reasoning, recommendation).

2) Write the spec before the next rewrite, not after the incident

Specs written post-mortem often become documentation. Specs written pre-build become design.

Keep it small. If it is too big to model-check, it is too big to be useful as a decision tool.

3) Model the failure moves as first-class transitions

Most systems model the happy path and then “handle errors.” That is not enough.

• What does “freeze” mean in state terms?
• How do you resume without double-applying actions?
• What does compensation look like, and what does it never touch?

This is the same mindset behind building AI rollouts that compound: you create a controlled path from current reality to target reality, with reversibility where possible. (Related: Build on the Stack You Have: The Rollout Pattern That Makes AI Compound.)

4) Turn invariants into runtime checks and runbooks

A spec that lives in a repo but never touches production behavior will be forgotten.

Pick 3 to 5 invariants and implement them as:

• Runtime assertions or guards at the boundaries.
• Alerts that page humans on invariant violation, not on noisy symptoms.
• Runbook steps that reference the invariant: what to check, what to freeze, what to replay.

5) Treat the spec as governance for change

Any change that affects the truth workflow should update the spec first. That is a lightweight form of change control that does not slow teams, it prevents expensive backtracking.

Budget overruns in software often come from building the wrong thing twice. The same dynamic applies here: ambiguity is a cost center. (If you want the broader governance angle, see Budget overruns are rarely a surprise. They are a governance choice.)

My take: AI will not remove the need for specs. It will raise the price of not having them.

There is a tempting idea in the background of the current AI wave: that models will write the code, and maybe even verify it. Wayne touches on whether AI could bring formal methods into the mainstream, and I agree with the direction but not the lazy interpretation. (See the interview.)

If AI makes it cheaper to produce software, it also makes it cheaper to produce subtle failure modes. Agentic systems multiply side effects. Distributed systems multiply interleavings. Together they multiply the number of plausible narratives during an outage.

Formal specs are how you keep one part of the system boring. Deterministic. Auditable. Recoverable. That is not a luxury. That is the foundation that lets you move fast everywhere else.

Use TLA+ where “we can’t tell” would become your worst incident. If you cannot explain the state, you do not own the system.

That is my opinion, and I have yet to see a team regret making the truth workflow legible.