It's kind of hopeless to try to prove that a microprocessor works according to spec, since you're dealing with physical objects in the real world. For instance, early versions of Intel's 386 processor had a 32-bit multiply problem that only showed up in some chips under particular combinations of temperature, voltage, and frequency, probably due to a transistor that wasn't large enough to provide an electrical margin under worst-case conditions.
Chip makers would disagree. They use tools that simulate at the electrical circuit level for just such problems, and using massive amounts of testing and inspection to statistically bound variations in chip geometry caused by process variation.
It is the quantum effects that occur at tiny geometries that make this hard, but every chip you buy has passed extensive variation.
To account for individual variation and random glitches there are other techniques, like triple modular redundancy or lockstep processors. Or for less stringent software, just computing it twice in different cores and memory blocks.