>why would the formal verification be any more correct than the program it is verifying?
It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.
Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.
It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.
Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.