The general idea is that formal methods are self-verifying, up to a point. Sloppy formal methods simply won't prove.

The point up to which formal methods stops is: do the formally encoded requirements actually encode what I want to be true?

One can make the argument that the requirements is a much smaller surface to verify than that of the entire program.

The counter argument is that figuring out what you want the program to do has always been the hardest part of programming, and that programming in itself is a journey to discover latent requirements.