[_ouml_]

Yes, these systems are being used to formally verify implementations of cryptographic protocols, or implementations of numerical algorithms, for example.

Note that there are two distinct components that interact: (i) verification of proofs and (ii) automation of finding the proofs. The latter is very much an active field of research, but so far isn't of the level that it will prove most of your theorems for you.