AI-assisted coding makes implementation faster, but systems remain just as difficult to reason about. A booking system can still over-allocate capacity. A retry can still apply an operation twice. Two services can still disagree about who owns a piece of state.
In What I Lose When AI Writes the Code, I wrote about how delegating implementation changes my understanding of it. As first drafts become cheaper, I want more engineering effort to go into explicit properties, independent models and tools that search for counterexamples.
I use practical formal methods broadly here. Fuzzing, property-based testing and model-based testing are testing techniques; Alloy and TLA+ work with formal specifications. All of them turn an informal claim into something a tool can challenge.
Cheap code shifts the bottleneck
Stanford’s 2025 AI Index reports that the price of querying a model at roughly GPT-3.5-level MMLU performance fell from $20 to $0.07 per million tokens between November 2022 and October 2024. That figure measures inference rather than a completed task, but neither price nor token count says whether the resulting code is correct.
An invariant offers a more stable reference point:
confirmed_bookings <= available_capacity
The property survives changes in models, prompts and implementation details.
Generated tests can share the implementation’s mistake
An agent can generate many tests without providing an independent test oracle. If I ask it to implement cancellation semantics and then write tests from the same prompt and repository context, one misunderstanding can appear in both. Every test may pass while the intended rule remains untested.
I state the expected behavior separately:
a cancelled booking cannot become active again
retrying a command cannot apply its effect twice
two exclusive allocations cannot overlap
An independent oracle can come from a domain rule, protocol specification, state diagram or operational limit. Generating more inputs helps only when it can recognize a bad result.
Match the technique to the uncertainty
I choose among these techniques based on what needs to vary:
| Technique | What it explores | Useful when |
|---|---|---|
| Example-based test | Named inputs and paths | A requirement or regression has a specific, readable example |
| Fuzzing | Mutated, coverage-guided inputs | Parsers, decoders and API boundaries must survive unexpected data |
| Property-based testing | Generated structured values | An invariant should hold across a large input domain |
| Model-based testing | Generated command histories | Correctness depends on lifecycle, retries or ordering |
| Model checking | Abstract states and transitions | A bounded design needs systematic exploration of safety or liveness |
They complement one another. Executable tests exercise production code; a model checker explores the specification within a bound.
Alloy fits structural problems such as relationships, ownership and constraints. TLA+ describes concurrent and distributed behavior; its TLC model checker checks safety and liveness over reachable states.
One invariant, four levels
Apply the capacity invariant at four levels.
An example test can reserve the final unit and assert that the next request fails. A property test can vary capacity, booking counts and cancellations. A model-based test can generate histories of creation, confirmation, cancellation and retry, comparing the service with a smaller state machine after each command.
A model checker asks whether any permitted ordering lets two clients confirm the final unit when messages may be delayed or retried. It can omit HTTP, database schemas and workers while retaining the states and transitions that determine the answer.
Model checking can expose a design flaw before the service exists. Model-based testing can compare the implementation with a simpler model. A regression test can preserve the concrete history that failed. None is complete: a specification may omit production behavior, and a test adapter may map an observation incorrectly. Their value comes from comparing representations built for different purposes.
For a concurrency-sensitive design, a small model is often cheaper than reworking handlers, APIs, tests and integrations. The service may need queues, caches, retries and a database; the design question may need only four states, three actions and one invariant.
AWS engineers have used specification and model checking since 2011 for difficult design problems in critical systems, as described in How Amazon Web Services uses formal methods. Their account notes a limit: verifying a high-level design does not prove that the implementation conforms to it. Executable tests, production assertions and telemetry help bridge that gap.
A risk-driven workflow
I start with the failure rather than the tool:
- Name the expensive failure. Prefer over-allocation, duplicate effects or stale authorization to “the system should be reliable.”
- Write an observable property. Describe what a caller, downstream service or operator can verify.
- Build an independent oracle. Use an equation, reference implementation, state machine or specification that does not reuse production decision logic.
- Choose the cheapest useful search. Use examples for known cases, fuzz weak boundaries, generate values or histories for broader invariants, and model-check designs dominated by interleavings.
- Preserve counterexamples. Turn a minimized input or history into a readable regression test and, when needed, correct the model or requirement.
- Review the oracle. Look for ambiguous state, missing transitions and unrealistic bounds.
Not every feature needs a formal specification. The strongest techniques belong where failure is costly and examples provide poor coverage.
Where AI helps with verification
AI can draft a fuzz harness, generate property-test scaffolding, translate a state diagram into a first model, suggest invariants or explain a minimized counterexample. I can use those drafts while remaining responsible for what must be true, where to observe it and whether the model captures the expensive failure.
I am more cautious about delegating the oracle. Stanford’s 2026 AI Index reports large gains on agent benchmarks while noting that agents still fail roughly one in three attempts on structured evaluations. The rate will change, but a capable code generator is not an independent oracle.