this is how you end up with darcs as your version control system. It’s provably correct, but about 1 in 10 times it hangs forever and never terminates. Also it doesn’t implement branching because that’s out of scope for the model.

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

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.

I think you're mixing the result of implementation and the way something's implemented. Darcs relies on abstract theory which implemented didn't end up very performant or full of features. But it would be close to the same speed if it was implemented in terrible C. On the other hand you can write provable implementation of git with similar speed as the current one.