While proving code matches a spec is very helpful, it's only as helpful as the spec being "correct" from a "does what we want it to do" angle. For example, you

While proving code matches a spec is very helpful, it's only as helpful as the spec being "correct" from a "does what we want it to do" angle. For example, you could do a bunch of spec proving on CPUs, but you wouldn't catch something like Spectre if your definition of correctness didn't include "no information leakage can happen through timings on branch prediction". And even then! You need to have the right definition on that front! Having specs and formally proven code helps to make sure your code isn't prone to a certain class of errors (just like bounds checking/lack of raw pointers prevents another class of errors), but it's not a magical catch-all. Especially if you are in a space like cryptography where you're trying to assert negatives (that end up being held up by assumptions around feasibility of certain things)