The 2006 Surprise: Bug-free Software?

Details: By Max Hinkley; July 23, 2026

It’s been 20 years now since the news broke. In 2006, a small item of software news splashed across several outlets: a non-trivial security application, built for a U.S. National Security Agency experiment, had been independently tested and then used with zero reported defects. The project was called Tokeneer, and it controlled access to a protected area using smart cards, biometrics, certificates, and an audit trail. Despite the huge implications, that news item has had very little impact on how most of us do software development, even two decades later.

I remember being taught that bug-free software is impossible; that focusing too hard on reducing defects yields diminishing returns. This was stated by professors and reinforced in books and magazines about software engineering. The Tokeneer experiment didn’t mean software engineering had finally solved software defects. It did mean that a stubborn industry assumption deserved another look. We had become accustomed to treating defects as inevitable, then treating the resulting testing, patching, workarounds, incident reports, and support costs as the normal price of doing business. Tokeneer showed us that, for some systems at least, we could do considerably better.

A Serious Demonstration

The NSA commissioned Praxis High Integrity Systems to build Tokeneer as a controlled evaluation of its Correctness by Construction approach. The stated target was a secure experimental biometric access-control system meeting or exceeding Common Criteria Evaluation Assurance Level 5, on a seven-level scale.

Tokeneer was not a toy problem selected because it would make a good demonstration. The system had to decide whether an individual could enter a secure enclave, validate credentials and biometric information, operate a door and alarm, preserve security rules under abnormal conditions, and keep an auditable record. Getting the normal path right is rarely the hard part. The difficult work lives in the awkward combinations: expired certificates, failed readers, incomplete enrollment, revoked credentials, equipment faults, and a user who is standing in front of a door while the system is deciding what it can safely trust.

Praxis delivered nearly 10,000 lines of high-assurance code in a fixed-price project reported as taking 260 person-days. The later public account says the costs per line of code were lower than for traditional development methods, a claim worth treating carefully but not dismissing simply because it is inconvenient to conventional practice.

Tokeneer did not come from nowhere. Praxis had already applied related high-integrity methods to SHOLIS, the Royal Navy’s Ship Helicopter Operating Limits Information System, where software helped determine whether conditions permitted safe helicopter operations from a ship. The domain was different, but the engineering problem was familiar: certain mistakes were not acceptable, requirements had to survive scrutiny, and testing alone could not provide enough confidence.

That earlier work matters because it puts the 2006 Tokeneer announcement in perspective. Tokeneer was startling not because formal methods had suddenly produced a one-off miracle, but because a substantial defense-security application made the results visible enough that more of the industry noticed. The methods had a history; the news was that they had again delivered under conditions where correctness mattered. The NSA’s controlled Tokeneer experiment was prompted by Praxis’s demonstrated success on SHOLIS.

What “Zero Defects” Means

To be accurate, the result was zero defects found or reported during independent testing and subsequent use. This is not suggesting that no defect of any kind could possibly exist. However, given the spotlight on this project, the verification effort was certainly quite rigorous.

That distinction matters because software claims often become grander in retelling. A program can be correct with respect to one specification and still fail a need the specification forgot to express. Hardware can fail. Sensors can lie. Operators can misunderstand procedures. A secure access-control system can be perfectly faithful to its rules while those rules themselves turn out to be incomplete.

Still, zero reported defects in independently tested, non-trivial security software is extraordinary enough. The right response is neither “therefore formal methods make every system perfect” nor “therefore it was only a publicity exercise.” The result is evidence that a more disciplined development process can change the defect profile substantially, particularly where the requirements can be stated precisely and the consequences of failure are expensive.

Correctness by Construction

Correctness by Construction is a name for a development approach that tries to remove defects before they become executable code. Requirements, architecture, detailed design, code, reviews, analysis, and testing are treated as linked stages of evidence rather than as separate activities conducted by separate teams with separate documents.

The approach used SPARK Ada, a high-integrity programming language and tool environment. SPARK is designed to make certain properties amenable to static analysis and proof: absence of particular runtime errors, controlled information flow, well-defined data dependencies, and conformance of code to specified behavior. The programmer still has to think clearly. The tools do not replace that work. They make unclear thinking harder to hide.

That last point is the practical heart of the matter. Most defects that make it into the software are not caused by a programmer failing to type carefully enough. They begin earlier, when nobody has decided exactly what should happen in an exceptional state, when two requirements quietly contradict one another, or when a design assumes a condition that the real world does not reflect. Formal methods force some of those assumptions into daylight.

Formal Does Not Mean Impractical

“Formal methods” can sound like a demand that every programmer become a mathematician before being allowed near a keyboard. That reputation has been earned in part by the way the subject is sometimes presented. The mathematics is real, and some forms of proof are demanding. The practical purpose, however, is straightforward: describe important system behavior precisely enough that the description can be checked, reasoned about, and connected to the code.

The methods exist on a spectrum:

Formal specification describes requirements and system states using precise notation, exposing ambiguity before implementation.
Model checking explores a finite or bounded model automatically, looking for states that violate a required safety or security property.
Theorem proving constructs or checks mathematical arguments that a system satisfies stated properties, often with substantial human guidance.
Static analysis examines source code without running it, finding patterns such as unsafe data flow, possible runtime failures, concurrency errors, or violations of coding rules.
Contracts and annotations place preconditions, postconditions, invariants, and similar claims directly alongside code, so the program carries more of its intended behavior with it.
Type systems and restricted languages prevent broad classes of errors by making dangerous constructions difficult or impossible to express.

Some organizations will need the stronger end of that spectrum. A safety function in a medical device, avionics software, a cryptographic protocol, or a system governing access to sensitive facilities has a different failure budget from a typical business application. In those settings, discovering a defect after deployment may be unacceptably late.

Other teams can gain much of the benefit from less ambitious techniques: better specifications, executable assertions, static analysis in continuous integration, a strongly typed language, careful interface contracts, and a deliberate decision about which failures must never occur.

The Cost Argument Was Never Quite Complete

Formal methods have often been rejected on cost grounds. That argument generally counts the visible cost of specification, proof, tooling, training, and review. It typically disregards the cost of the defect that was not prevented: emergency releases, customer disruption, security exposure, operational recovery, regulatory attention, damaged trust, and the quiet diversion of good people into permanent cleanup work.

Tokeneer was designed in part to test the economics, not merely the technical feasibility, of high-assurance development. The published account reported that the work achieved lower cost per line of code than traditional approaches, while independently tested software and subsequent use produced no reported defects.

No one project establishes a universal cost model. Lines of code are not a complete measure of complexity, and a disciplined project with a stable scope will not resemble every troubled modernization program. Even so, the case challenges the casual claim that rigorous methods are automatically too expensive. Prevention costs money. So does failure. The difference is that prevention is usually budgeted in advance, while failure arrives later disguised as an emergency.

A Better Question

Not every application deserves full formal proof. Most do not. Pretending otherwise would be dishonest.

In deciding whether formal methods are justified, and at what level, the question that should be asked is: Are there properties of this system important enough that we should not rely solely on testing to discover violations?

Testing is indispensable. It’s ubiquitous, and it’s easily understood; but it’s too expensive and too weak to be our primary mechanism for establishing that critical code is free of whole classes of defects. Where requirements can be stated precisely, formal methods should be used to prove the absence of those defects. Testing should then concentrate on what proof does not settle: the correctness of the toolchain, the validity of assumptions, integration with hardware and external systems, operational behavior, performance, usability, and whether the system solves the actual problem.

Another point is often missed: lightweight formal methods, including contracts, annotations, and static analysis, can be used alongside heavier methods. Areas of an application that do not justify full proofs can still benefit from interface-level checking, including the kind supported by static analysis tools such as Splint.

Formal methods change the balance. They provide evidence about classes of behavior that testing may sample only thinly or miss altogether. They are particularly valuable when the system has a clear set of critical properties, such as “unauthorized access must never be granted,” “a transfer must preserve value,” “a command may not place equipment in an unsafe state,” or “private data must not reach this output.”

SHOLIS and Tokeneer demonstrated what sound engineering judgment can accomplish when correctness is approached with discipline as an achievable design objective, rather than something that is accomplished solely as the result of exhaustive testing. That was the shocking news in 2006. In 2026, it still has not been given the recognition it deserves.

Learn More: