Agree. Not something I know a lot about but it seems to be a significant undertaking. I figure a production-grade implementation in safe Rust is more likely than a verified implementation in SPARK.

I don't know how serious the rustls implementation is. Nice to see it makes no use of Rust's unsafe features.

https://github.com/ctz/rustls