[Cryptography] Has formal verification actually been useful in the real world?

[Henry Baker]

At 09:28 PM 3/10/2017, James A. Donald wrote:
>Has a complete formally verified system been deployed anywhere?
>
>Is there one keeping the electricity grid up?
>
>Or a formally verified browser?
>
>Or even software for converting graphics files to images on the screen so that a broken image will not take control of your computer?
>
>Back in the days of usenet there used to be an old and obscure unix based usenet browser that would crash on unusual control character sequences and start executing usenet post text as machine code.
>
>Is there any proof that that cannot happen with unusual html or graphics?

It is my understanding that subsequent to the Intel "Pentium" floating point bug, Intel has always formally verified its arithmetic (at least the floating point arithmetic).

It's also pretty obvious that Intel has NOT been formally verifying its address translation or caching systems, as they have been enabling huge numbers of papers describing attacks on them.