Earlier quoted context omitted.
I've got a strong background in formal verification. I do not believe that "formally verified" means "security bug free". In fact, I personally know researchers who have had vulns found in their formally verified code more than a decade after they completed the verification.
I agree, there are lots of outrageous claims out there about "provably secure software" which seem very dubious. What are your thoughts on SEL4, is it really a breakthrough it is made to be in success of formal verification? Is there a way for users/administrators deploying it to verify themselves authors' claims? Or is it too difficult? I am afraid the latter... In 2004 Peter Gutmann in his thesis/book criticized th…
Breakthrough? No. Good work? Yes.