One in Nine Billion

In the summer of 1994, a mathematics professor named Thomas Nicely was computing the sum of the reciprocals of twin primes — the kind of patient, unglamorous calculation that runs for months and interests almost no one. His numbers kept coming out subtly wrong. He checked his code. He checked his libraries. He checked his machines against each other. By October he had isolated the culprit, and it was not software. It was the flagship processor of the largest chip company on earth, returning incorrect answers to division problems.

The Pentium’s divider carried a lookup table with a handful of missing entries — five cells, out of more than a thousand, that should have held values and held nothing. On almost every division ever performed, the omission didn’t matter. On roughly one input pair in nine billion, it did: the chip returned an answer that was wrong from about the fourth significant digit. Not garbage. Not a crash. An answer that looked exactly like a right answer and wasn’t.

Here is the detail worth sitting with: the chip had passed its tests. Intel was not careless — its verification suites ran millions of cases, and every one of them came back clean. The flaw survived because testing is sampling, and the bad inputs lived in the part of the space no sample visited. When the story broke, the company first argued the odds — a typical user might hit the bug once in twenty-seven thousand years — and discovered that spreadsheet users do not experience probability that way. The recall cost $475 million, and the industry learned to say the words formal verification out loud.

An input space, sampled. Every dot an input a test could visit; the flaw lives where no test looked.

The deeper lesson was never really about one chip. It is about what a passed test actually asserts. A test suite proves a system was not wrong on the inputs tried. It says nothing about the inputs not tried, and for any interesting digital system the inputs not tried outnumber the atoms in the building. In continuous engineering this gap is survivable — a bridge that holds at ninety-nine load points will hold at the hundredth, because the physical world interpolates. Digital systems do not interpolate. They are exact, discrete, and cliff-edged, and almost right is not a lesser degree of right. It is a specific way of being wrong that has chosen its hiding place well.

Thirty years later, this is still how the infrastructure of the networked world is certified. A vendor implements a specification. A conformance suite — a sample — is run against it. A badge is issued. Two devices bearing the same badge are then presumed to behave identically, and mostly they do, until traffic finds the corner where they don’t: the malformed packet handled two ways, the timer that one implementation rounds up and another rounds down, the boundary case two engineering teams read differently in the same paragraph of the same standard. These divergences are not hypothetical. They surface in production, between vendors, years after deployment, and they are found the way Nicely found his — by someone noticing that the numbers are subtly, patiently wrong.

And when the divergence surfaces, there is no good way to settle it. You cannot read the competing designs; they are trade secrets. You cannot exhaust the input space; it is astronomical. You can only run more samples, argue about the standard’s prose, and negotiate. The industry’s deepest behavioral guarantees rest, in the end, on the same foundation that failed in 1994: we tried some inputs, and the ones we tried were fine.

The question that interests us is what it would take to do better — for a device to demonstrate, rather than sample, that its behavior matches a specification exactly; for two implementations to establish that they are the same machine in every case that matters, without either one opening its design to the other. The Pentium taught the industry that the gap between tested and true is real and expensive. It has not yet closed.

That is the space we work in. More soon.