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

[mok-kong shen]

Am 11.03.2017 um 06:28 schrieb James A. Donald:
> 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?

There is a paper G. Klein et al., seL4: Formal Verification of an OS Kernel:
www.cse.unsw.edu.au/~kleing/papers/sosp09.pdf

M. K. Shen