Proofs are useful -- because of their total coverage -- when verifying components that will be used in many different projects, like compilers, kernels and libraries, and even then only when they are sufficiently small to be doable within, say, 5-10 years by a dedicated team. A one-time gigantic job will pay for itself by being used (and hopefully paid for) by many customers over many years.
I think I also have a different conception of proof than you're naming. You don't need to prove your entire program. 10 small proofs strung together can go an enormous distance with low weight.
I have a very small sub-algorithm that I might try proving in TLA+ just to see how it goes.
[1]: I couldn't find the original TLA+ proof online, but the author of the Raft protocol said that he struggled even with partial machine-checked proofs.
People prove specific algorithms (distributed, concurrent or sequential) with TLA+, but once the spec is of a real system, things get much, much harder to prove.
There are model checkers that work directly on implementations, like NASA's JPF.
> I personally don't confer that much trustworthyness to systems that appeal to model checking tools for their correctness.
Given that the going rate for proofs is roughly 1-1.5 days per one line of code, which grows superlinearly with the code size, I think we have no choice...
In any event, pretty much all safety-critical software that human lives depend on (even many, many lives) is verified with model-checking in the best case. Use of proofs in verifying safety-critical systems is very rare, as even those domains can rarely afford it.
Also, remember that no one really needs 100% proof, as no other, non-software component in the system guarantees 100% reliability (not that model-checking can give us probability bounds).