I don't have hard numbers to prove it. But I think it's significant that https://deepspec.org/main, the largest recent formal verification project (at least in the US) chose to use Coq, which is based on type theory. There's also Coq-verified code in Chrome (http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP1...), a claim that can't be made for any other theorem provers (as far as I'm aware).