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 problem

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.