What’s important is to prove useful, high-level properties derived from the specs. The specs of program behavior are just the price of admission.

I agree. It’s kind of like secure boot, in reverse: the high level stuff has to be complete and correct enough that the next level down has a chance to be complete and correct.