As I said in a similar post, their proofs show that their implementation is logically correct--their implementation will behave according to their formalization

As I said in a similar post, their proofs show that their implementation is logically correct--their implementation will behave according to their formalization of the RFCs. This says nothing about how secure it is with respect to side-channel attacks. For example, they admit that they did not model time in their proofs, so they have NOT proved that they are immune to timing attacks. Moreover, F# runs on top of the unverified CLI--bugs in the CLI can be used to break miTLS.