I want coding agents to take on more of the implementation. I also want to understand what I’m accepting when they come back with a result. Writing a spec gives those decisions somewhere to happen, but it gives me another set of files to keep current too.
In this episode, I revisit the trade-offs around spec-driven development and the fear that the requirements, tests, and code start describing different behavior. In the cart-policy example with IBM Bob, changing the design from 30 to 90 days left the old tests green and every requirement ID connected. Well, the links were intact. The new decision hadn’t reached the assertions.
Then I go through the Java inventory experiment with TLA+ and Lean. A model checker found the sequence that let two callers reserve the last item. A separate proof checked the arithmetic rule. Neither check proved that the Java implementation matched its formal definition, so the tests and the review of that connection stayed part of the process.
I also consider how this changes as models become more capable. Needing fewer instructions about the implementation doesn’t settle the business rule or tell me which checks are enough to accept a change.
The episode is narrated locally with Qwen3-TTS and my trained LoRA voice adapter.
Chapters
00:00 — Intro
00:10 — What I want from specifications
01:37 — The cost of vague specs and the maintenance of detailed ones
04:05 — IBM Bob and the cart policy: 90 days in the design, 30 days in the code
07:07 — How specifications and code drift apart
09:31 — One item, two callers: trying TLA+ and Lean with Java
13:23 — What the formal checks prove, and what they leave open
15:46 — What better models could change
19:02 — What I’d keep for the next Java change
20:36 — Outro
Related articles
Why AI Coding Agents Still Need Clear Specs — The correction effort that follows a vague request, and how acceptance criteria can make the intended behavior easier to check.
Spec-Driven Development Needs an Exit Strategy — Small change briefs, the cost of keeping design prose current, and where lasting constraints belong after implementation.
Formal Verification for AI-Generated Java — The inventory example with Java tests, a TLA+ model, and a Lean proof, including the limits of each check.
