WireGuard is a recent and prominent example of a system that has been formally verified (https://www.wireguard.com/formal-verification/). There are implementations in a variety of languages due to integration considerations.

You will find at the bottom of that page C implementations of curve25519 that are proofed and derived from F* and Coq. Curve25519 is a relatively simple implementation and only one part of any system that uses it. As you can see in both of these implementations the papers recognize a team of contributors each - this should provide some insight as to the cost of such work. That doesn't make it unimportant, it just makes it rare.

Out of curiosity did the Wireguard formal verification effort end up identifying any security issues in the implementation?

Now that is interesting. I didn't know that and will have to look further to understand what it means.

Wireguard seems to be written almost entirely in C, is that right?

The symbolic proofs of the protocol are independent of the implementation. The portions of the implementation that are formally verified are written in F* and Coq, and emitted as machine-generated C.

> We have no ssl library written in a memory-safe, functional language that has been proven correct that has dominated the space. Heartbleed wasn't yesterday.

Heartbleed didn't affect https://hackage.haskell.org/package/tls even though it isn't formally verified.

Does anybody at all use that library in production at scale, ever? Genuine question. Maybe they do?

Why hasn't this really good result meant _everybody_ now uses that library by default and has to justify using something else?

There is something here not being discussed, what is it?

There's a hint it was used at Dell in some capacity 6 years ago, judging by this comment https://www.reddit.com/r/haskell/comments/5gyrdv/what_is_war... The thread discusses "warp-tls" which is a webserver extension that uses that "tls" package as a dependency for TLS support.

Ok but this is surely not compelling evidence of literally anything. Perhaps, in fact, the opposite. This is what we have for evidence and nothing more then WHY???

There is something here, at least one thing, that seems to be dominating outcomes, and is not being discussed.

Nobody has even a half-suggestion of what it might be and that is not making it (or them) go away as problems that are not being solved.

rustls isn't formally verified but no critical CVEs have been found in it yet. The only CVE is one DoS.

And I don't know about "used at scale" but we use it in production for Pernosco.