Formal proof of design correctness doesn't preclude technical flukes.
On the contrary, do you know the technological process to produce CPUs with varied speed and varied number of cores in the same family?
Make a single design. Manufacture exactly the same wafers. Test the built CPUs, stress-test their capacity to perform at varied speeds.
Surprise: the results vary wildly from chip to chip, made with exactly the same design, machine, process.
These made with less contaminants will perform better and be labelled higher speeds, these speeds tagged in firmware. These where all 4 cores work flawlessly will be sold as quad-core. These where 2 cores are definitely underperforming, will have them disabled in firmware and be sold as dual core. You can often make your CPU triple-core by enabling one of cores disabled by factory.
And the bottom line is the process of testing depends on luck - on the fact that the fault surfaces during the tests, and not later. That it's frequent enough to be noticed by the QA. That it doesn't appear in conditions obscure enough to be overlooked in test cases.
As result you receive a product that will perform correctly most of the time in conditions not too varied from test conditions. But it's full of potential faults, and bugs for which no software solutions exist - because they are unique to your singular issue of the CPU.
Of course there are bug-free CPUs. Manufactured with extreme redundancy, in a process suitable for CPUs of a thousandfold higher complexity. Except they are trivial too, each of the parts testable thoroughly. Modern Intels with byzanthine complexity of super-efficient optimizers built in, simply utilize every last nanometer of chip to fit more cache, more pipelines - they won't sacrifice half of the volume to features that will be used only during testing, to triple-check every single transistor.