That's not what I said, and it's not what we're talking about.
There's very little formally verified software out there, due to how challenging it is to use formal methods in large software solutions.
It makes little difference here whether the developer does it for a living. C codebases are prone to certain kinds of bugs that don't tend to arise when a safer language is used. We see a steady stream of these sorts of defects in FOSS C codebases and proprietary ones. Microsoft's closed-source TLS library has had similar issues, [0] as has Windows more broadly of course.
All that said, it would be great to see a serious and well-funded effort at a formally verified TLS implementation. Until then, we have the option of just using safer languages, but it's not getting much traction.
That's not what I said, and it's not what we're talking about.
There's very little formally verified software out there, due to how challenging it is to use formal methods in large software solutions.
It makes little difference here whether the developer does it for a living. C codebases are prone to certain kinds of bugs that don't tend to arise when a safer language is used. We see a steady stream of these sorts of defects in FOSS C codebases and proprietary ones. Microsoft's closed-source TLS library has had similar issues, [0] as has Windows more broadly of course.
All that said, it would be great to see a serious and well-funded effort at a formally verified TLS implementation. Until then, we have the option of just using safer languages, but it's not getting much traction.
[0] https://signatures.juniper.net/documentation/signatures/SSL%...