This reframes the whole conversation. If implementations are cheap to regenerate, specifications become the durable artifact.

Something like TLA+ model checking lets you verify that a protocol maintains safety invariants across all reachable states, regardless of who wrote the implementation. The hard part was always deciding what "correct" means in your specific domain.

Most teams skip formal specs because "we don't have time." If agents make implementations nearly free, that excuse disappears. The bottleneck shifts from writing code to defining correctness.