Prose as Code: Applying Formal Verification to Product Specs

When a developer starts working from a product spec, they usually ask questions like: What persists across a retry? Who owns a half-finished operation? How does a failed state get out?

Spec validation is a standard step in agentic workflows — BMAD runs the spec through a master checklist, and most pipelines have an equivalent gate. But the checklist is written before it inspects any document. The checklist only asks whether the sections are filled and whether the spec and the architecture agree. The developer’s puzzling questions (mentioned above) came from the specific document he examined. An agent is rarely puzzled. It meets the missing rule, picks a plausible default, and keeps going, so the decision nobody made travels through every stage that follows:

The last stage is the trap, and only the end user is left to catch the invention.

A Formal Verification Primer

Consider a parcel-locker flow:

• A courier scans a parcel, places it in a compartment, and closes the door.
• The system marks the parcel “Stored”, generates a pickup code, and sends it by SMS.
• The recipient has 72 hours to collect it.
• A nightly sweep marks overdue parcels as “Expired”.

It reads like a complete happy path. Let’s walk the system states:

• The door closing is physical and largely irreversible. Code generation and SMS delivery can fail after it. Does the parcel become “Stored” before a usable code exists? Does the 72-hour clock start even though the recipient cannot collect the parcel? That is an atomicity problem: the product presents one operation, and the world can observe several partial outcomes.
• The “Expired” status. If the parcel stays in the compartment and the spec names no return operation, every expiry permanently consumes a compartment. The state exists; its continuation doesn’t. That is liveness: once the system enters a state, is there a defined way forward?
• The 72-hour promise doesn’t align with the nightly sweep — enforcement can land anywhere from hour 72 to hour 96. Either reject the code at the exact deadline or state the promise as “72 hours, enforced at the next nightly sweep.” That is consistency and enforceability: a stated guarantee the mechanism underneath can’t actually keep.

Atomicity, liveness, consistency, and enforceability: these four ideas make useful review lenses:

• Atomicity: Can an operation leave a partial result?
• Liveness: Does every valid state have a way forward?
• Consistency: Do shared rules hold across operations, states, and surfaces?
• Enforceability: Can the mechanism actually keep the product promise?

Formal Verification makes related questions precise: what must never happen, and what must eventually happen.

I work as a Product person with a software engineering background, and I’d been reading specs this way for years before I had names for any of it. Later, while working on DeFi smart contracts, I met Formal Verification through tools like Certora and wrote an article explaining the scientific vocabulary.

The rigor of formal methods, combined with an LLM’s ability to read ordinary prose, makes this mindset usable in an agentic workflow.

From Tests to Formal Verification to Product Prover

Tests check selected scenarios. Formal Verification starts with a system model and rules the model must never break. Instead of checking specific examples, it asks whether any allowed sequence of events can break one of those rules.

I built Product Prover to apply that habit to ordinary prose. It reconstructs an approximate state machine from the document, looks for counterexamples, and returns the missing rules in plain product language — the same move once made for code can process a text document (namely the product spec) the code is generated from!

Prover Lenses as a Part of Agentic SDLC

The method operates through reusable review lenses, sweeping the document for types of systemic structural failures:

• Atomicity: Can a unified operation fail midway, exposing a partial state to the outside world? For instance, a system charges a card but crashes before generating the receipt, leaving an orphaned transaction.
• Liveness: Is there a guaranteed path forward from every state, or might the system get stuck in an unplanned end-state forever? If a parcel is marked “expired” but the spec lacks a return flow, the compartment is permanently bricked.
• Consistency and Enforceability: Can the underlying mechanism actually keep the product promise? For example, requiring a strict 72-hour expiration limit while another part of the spec states the cleanup sweep must run only once a night.
• Unwritten Seams: When features are described in isolation, what happens when they potentially share the same resource? A classic case is a payment overlay colliding with a sudden session timeout banner on the same screen.
• Paired-transitions: Is there an exit for every entry state (like open/close or lock/unlock)? Asymmetry is acceptable, but it must be an explicit, documented decision rather than a forgotten teardown flow.
• Self-triggering Observer: Can a component reacting to an event accidentally emit that same event? For instance, an automation bot leaves a “processed” comment, which updates the ticket’s activity timestamp and forces the bot to process it again.
• Completeness of Sets: Does the spec explicitly handle all possible values in a category? For example, when a system defines five enum statuses but describes the flow for only three.

Gaps already marked TODO in the product spec appear separately as acknowledged issues; they do not count as newly discovered defects.

Heads-up: a concrete Product Prover run follows later.

Where the Review Fits

Product Prover is a part of my own agentic workflow. The diagram below shows where it is used in the pipeline:

Product Prover currently ships as a Claude Code skill: reusable instructions and reference material that guide the agent’s review. The Prover can also be incorporated into Codex, Cursor, BMAD, or a custom pipeline; the surrounding system decides whether a defect blocks planning, files a spec-repair task, or lets agents repair and re-review automatically.

Surprisingly, applying the Prover directly to code works too.

With a spec beside it, that run is the ordinary document pass, using the code to check the pins — a pin being a file:line citation showing where a claim in the document is actually carried in the code. That’s how the Prover catches a spec that no longer describes what shipped.

Without a spec, the defaults live only in the code and may never have been a deliberate decision. A separate code mode then takes over, and two structural lenses still do the work:

• Class-Based Sweeps: when a defect is found, is it the only one of its kind? The Prover looks for the same bug pattern everywhere else in the codebase. For example, one installer script forgetting to quote a path means its four sibling installers are worth reading before anyone calls the bug fixed.
• Completeness of Sets: the code itself declares closed sets — an enum, the arms of a switch, a family of files meant to mirror each other. Does it handle every member, and where it handles one differently, does the code say why? Add a sixth status to an enum, and a switch covering five compiles fine and silently drops the sixth.

What the Run Actually Looks Like

A controlled demonstration: the excerpt below is deliberately incomplete, and Product Prover v4.3.0 reviewed it in FULL mode. These are the same three problems walked through by hand earlier in this article — the difference is that nobody pointed the skill at them.

The input spec and complete review are available in the repository.

The Spec Excerpt

Deposit

• The courier scans the parcel and selects an empty compartment.
• The locker opens the compartment. The courier places the parcel inside and closes the door.
• The locker controller marks the parcel Stored.
• The system generates a pickup code and sends the code to the recipient by SMS.

Collection Window

• The recipient has 72 hours to collect a stored parcel.

Expiry

• The nightly sweep marks a stored parcel Expired when its collection window has elapsed.

What Product Prover Wrote

The excerpts below are shortened. Each finding cites the rule at issue, traces the failure it permits, and proposes the missing behavior. The complete input and full review are available in the repository.

Assessment: needs significant rework. The flow is legible, but it publishes its main state before the recipient has a usable collection path; collection and expiry have no complete end state; and a nightly job cannot enforce an exact 72-hour promise.

F1 — Stored is entered before the collection path is made usable

“The locker controller marks the parcel Stored. The system generates a pickup code and sends the code to the recipient by SMS.” — Deposit, steps 3–4

If code generation or SMS queuing fails after Stored is recorded, the recipient has a parcel that appears stored but no usable way to collect it. Support sees a missing-code complaint while the locker remains occupied.

Add either a CodePending state with a recovery path, or move Stored until after a pickup code is durably recorded and delivery has been queued.

defect · partial-success-risk (atomicity)

F2 — An expired parcel has no defined operational exit

“The nightly sweep marks a stored parcel Expired when its collection window has elapsed.” — Expiry

An operator can see an expired parcel occupying a compartment but has no specified action, owner, or endpoint. The compartment can remain unavailable indefinitely.

Add an Expired → ReturnPending → Returned or Expired → ReadyForOperatorRemoval flow. Name the actor, removal deadline, recipient notification, and condition that releases the compartment.

defect · no-exit (dead-end)

F3 — A nightly sweep cannot enforce a 72-hour collection promise

“The recipient has 72 hours to collect a stored parcel.” — Collection Window

“The nightly sweep marks a stored parcel Expired when its collection window has elapsed.” — Expiry

A parcel that reaches 72 hours just after the nightly sweep can remain collectible for almost another day. The system therefore breaks its own customer-facing promise.

Enforce expiry at stored_at + 72 hours when a code is validated; keep the nightly sweep for cleanup only.

defect · unenforceable-promise (discharge)

The resulting spec clauses

• A parcel enters Stored only after its pickup code is durably recorded and a notification has been queued; otherwise it remains in a recoverable CodePending state visible to operators.
• At stored_at + 72 hours, the pickup code cannot open the compartment. The nightly sweep may clean up overdue parcels but does not extend collection eligibility.
• A parcel enters Collected only after the door closes and the locker confirms the compartment is empty; that transition invalidates the pickup code and releases the compartment.
• Every Expired parcel has a named operator-owned transition to return or removal, with a deadline and a recipient-notification policy.

Those four clauses are the actual output. Not “consider adding a return flow” — a state, an owner, a deadline, and the condition that frees the compartment, each one written so a developer or an agent can build against it.

What Kind of Assurance the Prover Provides

The LLM reading is probabilistic. Product Prover is not a mathematical theorem prover and cannot guarantee that a spec is complete or correct. Its value is a structured review: findings should trace each claim to the document, distinguish defects from acknowledged gaps, and propose repairs without inventing facts.

Charming enough, the skill never says “formal verification” anywhere. Tell a model it’s an expert in something and it starts sounding like one — jargon, definitions, a lecture where a review was wanted. What actually does the work: a finding should name who is affected, what triggers the malfunction, what exactly breaks, and what system state it leaves behind. Drop the words “formal verification”, and nothing changes. Drop the lenses, and the prover review turns into generic advice.

It was encouraging to find adjacent work pointing to a similar direction: ALICE pairs formal logic with LLMs to detect contradictions in requirements. A Ford patent application describes an LLM that judges whether a natural-language requirement is atomic and refactors it into a requirements language. Different systems, one direction: natural-language requirements are becoming machine-readable engineering inputs.

Conclusion and Next Steps

Аs an open-source project, Product Prover is useful in multiple agentic workflows. Try the method on real specs and adapt it to your delivery systems! The result (as I see it) is fewer “accidental” product decisions inside implementation agents, fewer tests confirming hallucinated defaults, and a specification that can take part in its own repair loop. Bad specs become bad code; catching the gaps before implementation means fewer bugs later.

For the full formal machinery, read the series: The Verifiable Spec (forthcoming).

When humans wrote code, finding such edge cases in product specs required senior intuition and collective review. Now that agents generate systems directly from prose, the spec is the first artifact that compiles. Everything built downstream is only as sound as the spec it was built from.