The point is that specifying and verifying requirements is a lot of work. It takes time and resources. This work has to be reused somehow.
We haven't found a way to precisely specify and verify requirements using only natural language. It requires formal language. Formal language that can be used by machines is called code.
So this is what leads me to the conclusion that we need some form of code reuse. But if we do have formal specifications, implementations can change and do not necessarily have to be reused. The question is why not.
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.