Why the industry’s most effective quality techniques are decades old, nearly free, and almost never used
On 19 July 2024 the security firm CrowdStrike shipped a configuration update to its Falcon sensor, and 8.5 million Windows machines stopped booting. Airlines grounded fleets; hospitals postponed operations; broadcasters went dark mid-bulletin. It is generally reckoned the largest IT outage in history. Parametrix, an insurer that prices cloud risk, put the damage to the 500 largest American companies alone at $5.4 billion, of which at most a fifth was insured.
CrowdStrike published its root-cause analysis two and a half weeks later. The sensor’s content interpreter supplied 20 values to detection templates; a new template type declared 21 fields. The test template that validated the new type happened to carry a wildcard in the 21st field, so no test ever read past the end of the array. The first production rule that put a real value there sent a kernel driver reading unmapped memory, on every machine, everywhere, at once, because the update had also skipped staged rollout.
Chief among the remediations CrowdStrike promised was fuzz testing: feeding a program large volumes of random and malformed input and watching what breaks. Fuzzing was discovered in 1988, when Barton Miller of the University of Wisconsin dialled into a Unix system through a thunderstorm and line noise began garbling his commands and crashing his programs. He turned the accident into a class assignment, then a study. Deliberately random input crashed between a quarter and a third of every Unix utility his students aimed it at. The published remedy for the largest outage in computing history is three years older than the web.
CrowdStrike is not an unusual case. A small family of verification techniques shares the same history: invented decades ago, documented in public, cheap to run, spectacularly effective wherever applied seriously, and adopted almost nowhere. Fuzzing is one. Crash injection, deterministic simulation and formal specification are the others. The techniques are not obscure; every one of them is a free download with its evidence in the public record. The explanation for their neglect is economic, and it is worth working through, because the economics are about to change.
The evidence is not subtle
Start with the strongest existence proof in the industry. SQLite is the most widely deployed database on earth: it sits in every smartphone, every browser, most operating systems and a good share of cars. The library is roughly 156,000 lines of C. Its tests are 92 million lines: 590 lines of test for every line of product. The suite achieves 100% coverage at the modified condition/decision standard demanded of flight-control software, and its anomaly harnesses simulate power failure, full disks, memory exhaustion, I/O errors and deliberately corrupted database files. The result is a library trusted by billions of devices and maintained by three people. The arithmetic is the point: the harness took years to build, and then made every subsequent release nearly free to trust.
Deterministic simulation has an equally clean record. FoundationDB, a distributed database begun in 2009, is famous among practitioners for building its test rig before its product. Its designers wrote a simulator that runs an entire cluster, disks, network and clocks included, inside one deterministic process. A seeded random-number generator chooses each run’s misfortunes: partitions, torn writes, dying machines, clocks that lie. Any failure replays exactly from its seed. Ten thousand seeds a night amounts to decades of production bad luck. Kyle Kingsbury, whose Jepsen project spent a decade dismantling the consistency claims of commercial databases, declined to test FoundationDB at all, remarking that its internal testing was more rigorous than anything he could subject it to. Apple bought the company in 2015 and built iCloud’s storage services on it.
The technique is now spreading, but along a revealing path. TigerBeetle, a newer financial-transactions database, runs its whole cluster inside one process and injects faults at rates no production environment would ever supply, on an accelerated simulated clock. And FoundationDB’s alumni founded Antithesis, a company that raised $47m to sell deterministic simulation as a service; early customers included MongoDB and the Ethereum Foundation. Consider what that business is: a bet that the industry’s most effective testing technique is so unlikely to be adopted in-house that renting it out will sustain a firm. So far the bet is paying.
Formal specification tells the same story with older dates. TLA+, a language designed by Leslie Lamport for describing systems in checkable mathematics, has been freely available since 1999. A decade ago Amazon’s engineers reported in Communications of the ACM on using it across ten production systems. The specification of DynamoDB’s replication protocol ran to 939 lines and surfaced three bugs, one requiring a 35-step sequence of failures to trigger; the authors wrote that they were sure no review or conventional test would have found them. Engineers from entry level upward learned the language in two to three weeks, some in their spare time, unassisted. The cost is roughly that of the design document the team was going to write anyway. The difference is that this one can be checked by a machine instead of admired in a meeting.
The economics of unbought insurance
Why, then, does almost nobody do any of this? The immediate answer is that verification is insurance, and its payout is an event that does not occur. A quarter spent building a simulator produces no feature and no demo. The engineer whose harness prevented fifteen production incidents has, on paper, shipped nothing; the colleague who shipped the incidents along with the features has a promotion narrative. Management can see the features. It cannot see the incidents that never happened.
Markets have a name for this. George Akerlof’s 1970 paper on “lemons” showed that when buyers cannot observe quality, sellers stop supplying it. Software correctness is unobservable at the point of sale. The vendor that spends a third of its engineering on verification demos identically to the vendor that spends nothing; procurement prices them the same, so the discipline is pure cost until the outage arrives, and often afterwards too. CrowdStrike’s standard terms limited its liability to fees paid: a refund. Customers bore the $5.4 billion. When the seller does not carry the cost of failure and the buyer cannot see the investment in preventing it, the equilibrium is exactly the industry we have.
The clearest control group is hardware. Chip firms routinely spend more than half of all project effort on verification, and on many teams verification engineers outnumber designers, because a flaw that reaches silicon means a mask respin: millions of dollars, months of delay, no patch button. Software’s patch button set the perceived price of failure near zero, and practice followed the price. But some failures cannot be patched. Knight Capital’s manual deployment in 2012 reached seven of its eight servers; the eighth revived retired code and lost $460m in three-quarters of an hour. And a kernel driver that stops machines booting cannot be patched remotely, because a machine that cannot boot cannot fetch the fix. CrowdStrike’s update was undone by hand, machine by machine, across 8.5 million of them.
The bill arrives with the machines
By late 2024 more than a quarter of new code at Google was written by AI; the share across the industry has only risen since. When generating code becomes cheap, the binding constraint moves to verifying it. Human review was already a thin gate at human writing speeds; at machine speeds it is not a gate at all. The industry is about to discover that it automated the cheap half of software engineering and left the expensive half exactly where it was.
The old techniques are precisely the reviewers that run at machine speed. A fuzzer does not care who wrote the code. A simulator extends no trust and accepts no explanation; an invariant either holds across ten million seeded crashes or it does not. A firm that owns such a harness can accept machine-written code at the rate machines write it, and know what it has. A firm that relies on human attention must choose between throttling its machines and trusting them, and the market will not let it throttle for long.
None of this awaits discovery. Miller’s fuzzing paper is a free download. TLA+ has been free for 27 years. FoundationDB’s engineers explained their simulator from a conference stage in 2014, and SQLite’s testing regime is a public web page that reads like a dare. What they await is a buyer: someone willing to pay this quarter for the outage that never makes the news. A thunderstorm found the bugs in 1988, and the method has been free ever since. The industry has spent 38 years declining it.