I think the biggest reason is that most projects depend on an enormous mountain of software written in languages like C and C++, where we can't even be sure we

I think the biggest reason is that most projects depend on an enormous mountain of software written in languages like C and C++, where we can't even be sure we aren't indexing past the end of an array or casting a NULL pointer to the wrong type, let alone prove higher-level correctness properties. (To be fair, it's possible to generate C from a higher-level language/theorem proving tool, but few people actually do this.) For instance, most of us use operating systems, compilers, language runtimes, databases, web servers, web browsers, command line utilities, desktop environments, and so on written in not-terribly-safe languages. Formal verification might be worthwhile for its own sake, but for most projects you just need your own code to not be any more buggy than the rest of the technology stack you use, which you aren't going to re-create from scratch in a formally verified way because that's way too much work and the existing tools are just so useful and convenient and just an rpm/yum/git command away. The low-hanging fruit right now is to eradicate undefined behavior at all levels of the software stacks we use. This is a daunting task, but I think we'll get there eventually. Once we've banished heap corruption, segfaults, race conditions, and similar problems to the point where developers say "hey, I remember those things used to happen in the bad old days but these days I couldn't cause them if I tried" and we can be sure that if we call a function with the same input it will return the same result every time consistently, then is the time to consider formally proving that the result returned is correct. (That isn't to say that there aren't some domains now where formal methods are tremendously useful. Also, sometimes one can make a productivity case rather than a product quality case for at least using semi-formal methods; using a language with a strict type system can mean spending less time trying to resolve weird bugs.)