Nah, it's how you end up with HACL*: verified crypto that performs like C shipping in Firefox. https://github.com/project-everest/hacl-star https://github.com/

Nah, it's how you end up with HACL*: verified crypto that performs like C shipping in Firefox. https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star You can verify stupid designs or smart ones. You can do impractical verification or pragmatic approaches. Formal verification is a tool whose outcomes depend on who wields it. The only consistent drawbacks it has are requiring more expertise, the project takes longer, and the project has to be simplified in design/implementation. High-quality software in general (eg OpenBSD) often has same properties, though. Possibly intrinsic to achieving correctness rather than additional requirement of formal methods.