> Does formal verification lead to a strange-loop style or "It's verification all the way down" scenario, where you are shifting the correctness from the original code to the verification? Then must verify the verification ad-infinitum?

IANA formal methods guy, but my understanding is: yes, you're shifting the correctness burden from the code to the spec.

So why is that better? Because the spec is much shorter and more focused -- it strips out all of the implementation details.

It's bad to say "you have to trust this 100,000 line program." It's much better to say "you have to trust this 100 line spec, and the code that verifies it."

That is a great explanation!