But there's no CPU on the planet with a formal proof of its design.
Actually, formal proofs are used
extensively in the design of microprocessors. The need for this is something the microelectronics industry learned the hard way after the Pentium I floating point division bug.
And, yes, there has been at least one case of a completely proved microprocessor design. The reason we haven't seen more is presumably because
complete proof has turned out not to be necessary to achieve sufficient assurance of design correctness.