Aren't microprocessors Turing-Complete machines that undergo formal verification?

The kind of verification they undergo varies considerably. The amount of errata in modern CPU's shows both they're not fully verified for correctness and that the verification they get works wonders given number of components & interactions. Even if fully verified, the verification would be that the Turing-Complete hardware properly implemented a model of the Turing-Complete hardware.

That kind of buys us nothing in terms of whether we'll know if programs are malicious or contain them, eh? And look at the giant, losing game that followed between the mice and the well-fed cats. It's why safety-critical systems often used deterministic, state-machines running on simple MCU's or PLC's. :)