> A 15,000-line proof is going to have a mistake somewhere.

If this proof is formal, than it is not going to. That is why writing formal proofs is such a PITA, you actually have to specify every little detail, or it doesn't work at all.

> Verifying that those 15,000 lines do what they do doesn't give me much more confidence than thorough unit testing would.

It actually does. Programs written in statically typed languages (with reasonably strong type systems) empirically have less errors than the ones written in dynamically typed languages. Formal verification as done by F* is like static typing on (a lot of) steroids. And HACL has unit tests among other things.