I work in CPU design. So I'd add that the tools for formally verifying CPUs have come a very long way in the last two years, and the next two years look like they will be very exciting indeed.
There is a big overlap in prover theory. HOL Light comes from Intelite John Harrison.
I don't know much about CPUs, but I suspect that one of the core problems of software verification, the absence of a useful specification, isn't much of an issue with hardware.
