In 1994, a math professor named Thomas Nicely was running long calculations on his shiny new Intel Pentium computer and noticed his numbers were ever so slightly wrong. Not crash-the-machine wrong. Just quietly wrong, deep in the decimal places, in a way that only showed up for certain divisions. He’d stumbled onto a flaw baked into the silicon of millions of chips. Intel eventually took a charge of around $475 million to replace them.
That, roughly, was the price of a typo you couldn’t see.
I want to use that story, and two darker ones, to make a single point that sits at the heart of my field. It’s a point a computer scientist named Edsger Dijkstra made decades ago in one sharp sentence, and I’ll get to him at the end. The point is this: the way we normally check software can show us that bugs exist, but it can never show us that they’re gone. I’ll also cover some of the ways we can prove no bugs, and their uses in industry, at the end.
What actually went wrong inside the Pentium
The die of an Intel Pentium A80501 (66 MHz) — the original P5 generation at the center of the 1994 FDIV floating-point bug. (Pdesousa359 / Wikimedia Commons, CC BY-SA 3.0)
A computer divides numbers using a kind of built-in cheat sheet. To go faster, the chip doesn’t work out every division from first principles; it looks up partial answers in a table stored on the silicon, then refines them. This is the floating-point division unit, “floating-point” just meaning the way computers handle numbers with decimal points, like 3.14159, as opposed to integer numbers, like 23 or 34.
The trouble was that a handful of entries in that lookup table were missing. Out of thousands of cells, a few were blank where they should have held a value. For most divisions it never mattered. But for certain specific numbers, the chip reached for a blank cell and produced an answer that was subtly, confidently wrong, correct for the first several digits, then drifting off.
Here’s the part worth sitting with. Intel did test the chip, of course they did. But you cannot try every pair of numbers a person might divide; there are astronomically many. So you test a sample, a sensible, carefully chosen sample, and you hope it’s representative. The faulty entries lived in the space between the inputs they thought to try and the inputs people would eventually use. The bug wasn’t hiding from a careless team, the space needing to be checked was just far to large.
A rocket that trusted old code
An Ariane 5 on the ELA-3 launch pad at the Guiana Space Centre. The maiden flight, 501, tore itself apart seconds after lift-off — undone by a single line of arithmetic. (Philippe Semanaz / Wikimedia Commons, CC BY-SA 2.0)
On the 4th of June 1996, the European Space Agency launched the first Ariane 5, Flight 501. About 37 seconds after lift-off, it veered, tore itself apart under the aerodynamic stress, and self-destructed. No one was hurt, it was uncrewed, but years of work and a very expensive payload went up in smoke.
The cause was surprising in its smallness. Inside the rocket’s guidance system, a piece of software took a number describing the rocket’s sideways motion and tried to stuff it into a space of memory that was too small for it. In computing terms, a 64-bit floating-point number was being converted into a 16-bit signed integer, effectively squashing a space from 264 to 216. When the value was too large to fit, the conversion failed, called an integer overflow error.
The cruel twist: this code had been reused from the earlier Ariane 4. On Ariane 4 it was perfectly safe, because that rocket simply never moved fast enough sideways to produce a number too big for the container. Ariane 5 was more powerful. The same line of code, the same logic, met a flight it had never been designed for, and the number overflowed. The software wasn’t tested against the new rocket’s flight profile, because everyone trusted that working code stays working. It does, until the inputs change.
When the bug is measured in human lives
The hardest story is the Therac-25, a radiation-therapy machine used in the mid-1980s to treat cancer patients. It could deliver radiation in two modes: a gentle electron beam and a far more intense X-ray mode that was meant to be heavily filtered before it reached anyone.
The machine had a flaw of a particularly nasty kind: a race condition. That’s when two parts of a program run at the same time and the outcome depends on which one happens to finish first, like two people reaching for the same door handle and the result depending on split-second timing. If a skilled operator typed the treatment settings quickly and corrected them in just the wrong rhythm, the software could end up in a state where it fired the high-intensity beam without the protective filter in place.
Patients received radiation doses many times the intended amount. Several were seriously injured. Several died. The on-screen error messages were cryptic, the machine often seemed to say everything was fine, and because the fault depended on precise timing it was maddeningly hard to reproduce, which is exactly why ordinary testing kept missing it.
The pattern never went away
These three are the classics, but the same shape keeps reappearing in newer, larger machines. A few worth knowing — each one a rabbit hole if you want to follow the link:
Mars Climate Orbiter (1999). One team’s software spoke in pound-force, another’s listened in newtons. Each program was correct on its own terms; nobody checked the seam between them, and the $125M probe burned up in the Martian atmosphere. (NASA Mishap Investigation Board report)
The 2003 Northeast blackout. A long-dormant race condition froze the grid’s alarm software, leaving operators blind as conditions deteriorated around them. Around 50 million people lost power; engineers could only reproduce the bug afterwards by deliberately slowing the code down. (U.S.–Canada Task Force final report)
Knight Capital (2012). A botched deployment re-awoke a years-dead piece of test code on a single server. In 45 minutes it fired millions of unintended trades and lost the firm roughly $460 million. (SEC order)
Heartbleed (2014). A missing length check in OpenSSL let anyone ask a server for “a bit more memory than I actually sent you,” reading back passwords and private keys. It worked perfectly for honest requests — and catastrophically for a lying one. (heartbleed.com)
Boeing 737 MAX (2018–19). Often filed under “software bug” which caused several airplanes to crash and the loss of several hundred lives. The crashes were linked to the Maneuvering Characteristics Augmentation System (MCAS), which activated erroneously due to faulty angle of attack sensor data — a failure of design and requirements, not arithmetic. (That distinction, between a program that is correct and one that is correctly specified, is important enough that I’ll give it its own post.) (U.S. House Transportation Committee report)
What all of these share
Notice the common thread. In every case, the software behaved fine across the situations its makers thought to check. The disaster lived in the situations they didn’t: the unusual divisor, the faster rocket, the precise keystroke timing. Testing, by its nature, samples. It picks examples and tries them. And you cannot sample an infinity of inputs.
Which brings me, finally, to Dijkstra, one of the founders of how we think about programs, who put it better than I ever could:
“Program testing can be used to show the presence of bugs, but never to show their absence.”
Read that twice. It’s not a complaint about lazy testers. It’s a statement about a hard limit. No matter how many tests pass, including the proverbial ten thousand, all you’ve learned is that those particular ten thousand inputs were fine. The one that wasn’t on your list is still out there.
Why this matters
For most of computing’s history we’ve lived with this limit by testing harder, shipping fixes, and hoping the gaps are harmless. Often they are. But as software steers rockets, doses patients, drives cars, and increasingly makes decisions on its own, “we tested a lot and it seemed fine” is thin ground for safety-critical systems to stand on.
There is, it turns out, another way to ask the question. Instead of trying examples and hoping they’re representative, we can try to prove a property holds for every possible input at once, the way a mathematician proves a fact about all numbers without checking them one by one. That’s the discipline I work in, and it’s what this newsletter is really about.
This already works in the real world
If proving a program correct sounds like an academic fantasy, here’s the twist: it has quietly become industrial practice — often at exactly the companies whose failures we just walked through.
Start with Intel. After FDIV, “test a representative sample” stopped being good enough for arithmetic hardware, so Intel made mathematical proof a standard part of designing its floating-point units. Today it verifies that its divide, multiply, and square-root circuits return the correct answer for every possible input, not a sampled few — precisely because they don’t want another FDIV. The bug that opened this post is now one of the reasons the technique exists.
It has spread well beyond chips:
Amazon Web Services writes precise mathematical descriptions of how its core systems are supposed to behave, then uses a tool to check every possible ordering of crashes, retries, and network failures against them. On DynamoDB this caught a data-loss bug that only surfaced after a 35-step chain of events — something the team is convinced no amount of testing or code review would ever have found. A sister effort, “automated reasoning,” can now prove that a storage bucket can never be made public, rather than testing a few cases and hoping.
Airbus runs a tool called Astrée over the C code in its fly-by-wire flight controls to prove it can never hit a runtime crash — no divide-by-zero, no overflow, no out-of-bounds access — on any execution.
seL4, an operating-system kernel used in drones, cars, and defense systems, ships with a machine-checked proof that its code exactly matches its specification, making whole categories of crashes and security holes mathematically impossible.
CompCert, a C compiler trusted in avionics, comes with a proof that it will never mistranslate your program. A famous study that bombarded compilers with random code found hundreds of bugs in GCC and Clang — and none in CompCert’s verified core.
None of this means the software is perfect — every proof rests on assumptions, and pinning those down is its own craft. But notice what has changed. These teams are no longer saying “we tested it a lot and it seemed fine.” They’re saying “we proved it cannot do the bad thing” — and they can tell you exactly what “the bad thing” and “cannot” mean.
Next time, I’ll introduce the surprisingly simple idea that lets us talk about “every possible situation” a machine can be in, without listing them forever.
Further reading
The Pentium FDIV bug
Pentium FDIV bug — an accessible overview of the discovery, the lookup-table root cause, and the recall.
Cleve Moler, A Tale of Two Numbers — a first-person account by the creator of MATLAB, who helped build the software workaround.
Vaughan Pratt, Anatomy of the Pentium Bug — a rigorous analysis quantifying how rarely (and how badly) the flaw actually bit.
Ariane 5, Flight 501
Ariane 5 Flight 501 Failure: Report by the Inquiry Board (the “Lions report”) — the definitive official account of the overflow.
ESA, Presentation of the Inquiry Board report — the findings and corrective measures in brief.
Jézéquel & Meyer, Design by Contract: The Lessons of Ariane — why this was really a failure of reusing code without checking its assumptions.
The Therac-25
Nancy Leveson & Clark Turner, An Investigation of the Therac-25 Accidents (IEEE Computer, July 1993) — the canonical, careful reconstruction; essential reading.
Therac-25 — a clear summary of the race condition, the overdoses, and the lessons.
Formal methods in practice today
Newcombe et al., How Amazon Web Services Uses Formal Methods (Communications of the ACM, April 2015).
Byron Cook, Proving security at scale with automated reasoning — AWS’s “provable security” work.
Klein et al., seL4: Formal Verification of an OS Kernel (SOSP 2009).
Xavier Leroy, Formal verification of a realistic compiler (Communications of the ACM, July 2009) — the CompCert project.
John Harrison, Formal verification of floating-point arithmetic at Intel — how Intel proves its FPU correct after FDIV.