OpenSSL isn’t formally verified!?
No, neither is any part of your browser, your kernel, your hardware, the image rendering libraries that your browser uses, the web servers you talk to, or basically any other part of the system you use.
The closest to formally verified in your day-to-day life that you’re going to get may well be the brakes on your car, or the control systems on a jet engine. I shit you not.
We live on fragile hopes and dreams.
At lot of the internet is learning a lot more about how software in the wild functions after heartbleed. I found that statement to be one of the best summaries.
2 thoughts on “We live on fragile hopes and dreams”
I think the only bit of software that I know of that is formally verified is Knuth’s TeX.
TeX isn’t formally verified . On the other hand, Microsoft does formally verify third-party drivers .
Altran Praxis is a software company in the U.K. that has used formal methods on some safety-critical projects.