As people are discovering, natural language is insufficiently precise to be able to specify edge cases. Any language precise enough to be formally verified against is a programming language
Another agent: Code -> Inverted Spec
then compare Spec and Inverted Spec.
If there is a Gap, a Human fixes and clarifies the Gap.
This is like Generator and Discriminator aspects of GAN models or Autoencoder models.