The thesis is that you can come up with a tight spec that defines what correctness means for you. Then the AI writes lean proofs that your code follows this spec.
In practice, for real systems, this much moves source of truth, as you have pointed out.
However, there is a clear 'compactness' advantage for specs.
Specs can either define the operational (what it does) or the denotational semantics (what it is) for a system, while the code can only be operational. Some things are just easier and better defined in denotational semantics.
I’m not saying I’m right, but I want to understand. What’s the benefits of raw specs with AI, when AI can read the source of truth and explain to you?