Comment by zelly

Rustls is still not formally verified. It may not have memory errors, but there are a lot of other security errors besides just that (and there may be more of them since it hasn't been used as much as open|boringssl has been used). It's a slight improvement at best.

Ideally you want a formally verified SPARK or CompCert C implementation of TLS, but those are not open sores compilers so they won't fly.