I remember reading (~10 years ago) that F* was created as part of a "Project Everest" a long time back, with the goal of creating a provable TLS implementation. I never saw that anything came out of that though. If it's that hard to create something as well-defined as a TLS implementation, it seems futile to think this could ever be used for hand-wavy things we encounter in day-to-day work, no? Or are there real-world use cases where this could really be applied?