The Limits of Testing and Formal Methods — Another Way to Prove Absence

In Episode 1, we placed a single warning at the very origin of testing as a practice. Edsger W. Dijkstra, following discussions at the 1969 NATO Software Engineering Conference, wrote in his 1970 paper “Notes on Structured Programming” (EWD249):

“Program testing can be used to show the presence of bugs, but never to show their absence!”

Testing is nothing more than the outcome of running a finite number of inputs and paths. For a program with an infinite input space, testing can show that “no bug turned up in the cases tried,” but it can never guarantee that “there is no bug in the cases not tried.” This is not a problem that more careful testing can fix — it is a structural limit of testing itself.

This article traces the half-century of answers to that limit: formal methods, a family of approaches that describe a system in mathematically rigorous notation and mathematically prove or verify that the system satisfies its specification.

Where Testing Cannot Reach

Formal methods are not “testing, but better.” The two excel in different territory.

	Testing	Formal methods
Target	Running code	Specification (model) or the code itself
Nature of guarantee	Sampling-based	Exhaustive
Proving absence of defects	Not possible	Possible, conditionally
Cost	Relatively low to moderate	Relatively high
Strong domain	Integration, environment-dependent behavior, UI	Concurrency, protocols, distributed consistency

Formal methods are especially powerful for properties that are hard for testing to catch: concurrency bugs, distributed-system consistency, and protocol safety and liveness. In practice, teams commonly apply formal methods only to the core algorithms or protocols, leaving the surrounding code to conventional testing.

Model Checking — Exhaustively Sweeping Every State

Model checking models a system’s behavior as a finite state machine (or an abstraction of one), then exhaustively explores every reachable state to automatically verify that a specified property always holds.

The theoretical foundation was laid in the early 1980s by Edmund Clarke and E. Allen Emerson, and independently by Joseph Sifakis. The three shared the 2007 ACM Turing Award for this work.

The biggest challenge is the state explosion problem: the state space grows exponentially as the number of concurrent processes and the range of possible data values increase. To address this, techniques such as Ken McMillan’s symbolic model checking using binary decision diagrams (BDDs), and bounded model checking, were developed.

SPIN and TLA+ — Two Flagship Tools for Concurrency

SPIN, developed by Gerard Holzmann at Bell Labs, is a model checker specialized for concurrent systems. It uses the specification language Promela (Process Meta Language) to verify the safety and deadlock-freedom of communication protocols and multithreaded programs.

TLA+ (Temporal Logic of Actions) is a formal specification language developed by Leslie Lamport — a leading figure in distributed systems research, inventor of the Paxos algorithm, and winner of the 2013 ACM Turing Award. It is grounded in set theory and temporal logic, and describes a system’s state transitions mathematically. Its companion model checker, TLC, exhaustively verifies a model within a finite range. PlusCal, a pseudocode-like notation friendlier to programmers, compiles down to TLA+. Lamport laid out TLA+ systematically in his book Specifying Systems (2002).

Also worth noting: Alloy, developed by Daniel Jackson at MIT, is a lightweight language based on relational logic (built on first-order predicate logic) for describing data models and structural constraints; its companion Alloy Analyzer exhaustively explores every instance within a given scope and surfaces counterexamples. NuSMV, used for hardware and finite-state protocol verification, and CBMC, which targets C/C++ directly using SAT/SMT solvers, cover different layers of abstraction and are chosen depending on the task at hand.

AWS’s Practice — Finding Bugs Before Implementation

One of the best-known examples of formal methods paying off beyond academic interest, in actual industrial practice, is Amazon’s AWS teams’ use of TLA+. The paper “How Amazon Web Services Uses Formal Methods” by Chris Newcombe and colleagues (Communications of the ACM, 2015) reports that applying TLA+ to the design of core services including DynamoDB, S3, and EBS uncovered multiple subtle concurrency bugs — data inconsistencies that occur only under rare timing conditions — at the design stage, before implementation, bugs that would have been extremely difficult to find through testing or design review alone. It remains a frequently cited case demonstrating that “the correctness of large-scale distributed systems cannot be guaranteed by post-implementation testing alone.”

Theorem Proving — Writing the Proof Itself as a Program

Where model checking automatically and exhaustively searches a finite state space, theorem proving uses a more expressive logical system (higher-order logic, type theory, and the like) to construct a mathematical proof, often with human guidance. It can establish the correctness of systems with infinite state through a finite proof procedure.

Notable proof assistants:

Tool	Origin / key people	Theoretical basis
Coq	INRIA (France); foundational theory by Thierry Coquand and others	Calculus of Inductive Constructions
Isabelle/HOL	Larry Paulson at Cambridge; Tobias Nipkow at TU Munich	Higher-order logic
Lean	Leonardo de Moura, started at Microsoft Research, later supported by AWS and others	Dependent type theory

These tools rest on the Curry-Howard correspondence — the idea that “propositions are types, and proofs are programs” — which makes writing a proof mathematically equivalent to writing a program.

CompCert and seL4 — Proving “Zero Bugs”

Notable applications include CompCert, a C compiler formally verified in Coq by Xavier Leroy and colleagues, and seL4, a microkernel whose functional correctness was completely formally verified, announced in 2009 by NICTA (later CSIRO’s Data61), using Isabelle/HOL. These are among the rare cases in which it has been mathematically proven that “the core of a compiler or OS kernel contains zero bugs” — a level of assurance testing alone cannot reach.

Design by Contract — Eiffel’s Alternative Path

Design by Contract (DbC) is a design methodology introduced by Bertrand Meyer in 1986 through the language Eiffel, and it is a leading example of the “lightweight formal method” positioned between testing and full formal verification.

• Preconditions — conditions the caller must guarantee
• Postconditions — conditions the implementation guarantees after execution
• Invariants — conditions that must always hold throughout an object’s lifecycle

These are written explicitly into code as assertions and checked at runtime, so contract violations are caught immediately. Beyond Eiffel, similar ideas have been adopted in Java (formerly JML), Python (assert statements and the icontract library), Racket’s contract system, and Ada/SPARK, among many other languages.

The Front Line of Safety-Critical Systems

One of the earliest domains where formal methods became an institutional requirement, because human lives are directly at stake, is safety-critical systems.

Paris Métro Line 14 (Météor) is a well-known example: its driverless automatic train control software was developed and verified using B-Method, a formal specification notation devised by Jean-Raymond Abrial. Opened in 1998, this line is frequently cited as a landmark case of formal methods deployed in a real, large-scale commercial system.

SPARK, a subset of Ada augmented with pre/postconditions and dataflow contracts, can mathematically prove the absence of runtime errors such as out-of-bounds array access and overflow through static analysis, and is widely used in aviation and defense. DO-178C, the certification standard for civil aircraft software, demands rigorous development and verification processes; recent editions accept model-based development and formal analysis techniques such as SPARK as certification evidence.

Lightweight Formal Methods — A Third Path

Daniel Jackson coined the term lightweight formal methods for approaches like Alloy that “do not aim for a complete proof, but can find many bugs by exhaustively checking within a bounded scope.” This is an important distinction from “heavyweight” complete proof systems like Coq and Isabelle, one that helps balance adoption cost against payoff in practice.

Property-based testing belongs to this same lineage. It shares with formal methods the idea of formally specifying properties, but it differs from model checking by verifying through random sampling rather than exhaustive search.

Type Systems as an Everyday Formal Method

Static type systems, too, can broadly be viewed as a form of lightweight formal method. Type checking mechanically guarantees, at compile time and across the entire program, that a certain class of inconsistency (type mismatch) does not exist — the opposite of testing’s sampling-based nature.

However, type systems are limited to properties concerning “whether the types match,” and typically do not cover business-logic correctness or concurrency safety. In languages with dependent types (Idris, Agda, Lean, and others), types themselves can encode arbitrary logical propositions, so type checking can serve as a considerably more powerful proof mechanism.

A recent example of type systems becoming mainstream as lightweight formal methods is Rust’s ownership system and borrow checker. Through static compile-time checks, it guarantees the absence of memory-safety violations (such as use-after-free or double free) and data races — a formal-methods mindset built directly into a mainstream compiler.

Testing and Formal Methods: Complementary, Not Opposed

In most organizations, the practical approach is staged: use model checking first to cheaply flush out design-level errors, then apply theorem proving only to the core components that demand the highest level of assurance. SPIN and TLA+ excel at verifying the safety of concurrent systems and protocols; Coq, Isabelle, and Lean excel in domains — compilers, OS kernels — that demand extremely high assurance.

Dijkstra’s warning from Episode 1 does not condemn testing as a practice. It simply draws the line between “what testing can reach” and “what only mathematics can reach.” Over the following half-century, model checking and theorem proving have been steadily filling in the territory beyond that line — that is the conclusion of this article.

The next episode shifts the lens from “how do we verify” to “whose job is quality.” From dedicated testers to everyone’s quality traces how, beyond proving correctness, organizations came to share responsibility for quality — including performance and security — across every role.