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)

Given the current state of security practices, I'd say we're lucky if they have unit tests.

> One might hope you have a formal spec of a cryptographic library.

Which would be a good first step, but wouldn't protect against timing attacks or Spectre-like hardware frailties.

A solid start is better than nothing, but a false sense of security is worse than nothing.