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.
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.
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.