Isn't a sufficiently complete specification + proof with which to check generated code against just going to mean that a human spent exactly the same amount of time writing code as they would without the AI generation side of things?