alt Hacker NewsLCF-style provers like Isabelle/HOL and HOLlight are some of the most widely used, and oldest interactive theorem provers. If they consistently show smaller error rates than other systems, that is an interesting empirical observation. To give but one recent example: Amazon recently announced a vast 260000 lines of Isabelle/HOL-checked correctness proof of their new Nitro hypervisor for AWS EC2 Graviton5 instances.
LCF-style provers have a much smaller trusted computing base than Curry/Howard based provers like Coq, Agda and Lean.
One may wonder if there is a correlation between size of TCB and error rate in widely used provers?
> LCF-style provers have a much smaller trusted computing base than Curry/Howard based provers like Coq, Agda and Lean.
I'm not sure that this is correct. The TCB in a CH based prover is just the implementation of the actual kernel. In LCF, you also have to trust that any tactics are implemented in a programming language that doesn't allow you to perform unsound operations. That's a vast expansion in your TCB. (You can implement LCF-like "tactics" in a CH-based prover via so-called reflection that delegates the proof to a runtime computation, but you do have to prove that your computation yields a correct decision for the problem.)