A factory that survived its own failures, and the instrument it used to find the next one

A queue bug double-counted PR comments, so two sandboxes would race to conflicting commits; it was fixed and regressed across roughly sixty PRs in two or three days. What held was not another patch. The team built a Quint formal model of the queue's admission behaviour and checked every PR against it: "We've had absolutely zero recurrences of that after the fact." He says he would not have known how before agents, and that it took about a day. Then, at an offsite, they handed a coding agent only their verification layer, no source and no unit tests, and asked it to rebuild the orchestrator in Elixir. "Our queue was perfect, the queue works totally fine, so the formal model held up well there." Linear label routing, PR stacking and CI batching all broke, because each had only ever been covered by unit tests, and he called the experiment off. Neither failure account appears in the show notes.

Why it matters: Rebuilding a system from the verification layer alone turns the episode into a reusable test: whatever breaks is what that layer does not cover. The episode's throughput and human-review percentages are vendor self-report on the vendor's own podcast, tracked here as unverified and not used above.