I'm sure you encounter "high assurance code" like this every day -- your operating system, the secure protocol used to post your comment, the controls for your Anti-Lock Breaking System in your car.
TLS has been subject to lots of formal verification. The other things, probably not so much.
Verifying some (but not all) properties of crypto is relatively (but not absolutely) easy, because it's essentially just math with pure functions. Operating systems and physical controllers with real-time constraints have different requirements and more interacting state, which means that the desired properties are not easily expressed as a mathematical expression.
How much of those were formally proven?