Proving software correct rather than testing it and hoping.
9 topics · 16 curated works
No prior grounding assumed.
How Amazon Web Services Uses Formal Methods
Newcombe et al. · 2015
Reports that TLA+ specifications found subtle bugs in production distributed systems that code review and testing had missed, an argument for…
Assumes you know the vocabulary.
Social Processes and Proofs of Theorems and Programs
Richard A. DeMillo, Richard J. Lipton & Alan J. Perlis · 1979
Argues that mathematical proofs persuade because a community works and reworks them socially, a process formal program verification could not yet…
Primary sources and full treatments.
An Axiomatic Basis for Computer Programming
C.A.R. Hoare · 1969
Defines program correctness using pre- and post-conditions joined by inference rules, giving imperative programs the kind of proof mathematics…
+13 more at this level
12 of 16 works
Newcombe et al.
Reports that TLA+ specifications found subtle bugs in production distributed systems that code review and testing had missed, an argument for verification as an everyday engineering tool.
8 pageslink checked 17 Sept 2026Richard A. DeMillo, Richard J. Lipton & Alan J. Perlis
Argues that mathematical proofs persuade because a community works and reworks them socially, a process formal program verification could not yet replicate.
Assumes having seen a mathematical proof argued over by people, which is the process the paper is about
10 pageslink checked 17 Sept 2026C.A.R. Hoare
Defines program correctness using pre- and post-conditions joined by inference rules, giving imperative programs the kind of proof mathematics already had.
Assumes first-order logic and the idea of a proof rule; the programs themselves are tiny
5 pageslink checked 17 Sept 2026Gary A. Kildall
Frames data-flow analysis as computing a fixed point over a lattice of program facts, giving static analysis a single mathematical framework that every later data-flow algorithm is an instance of.
Patrick Cousot & Radhia Cousot
Formalises static analysis as computing an approximate, terminating version of a program's semantics over an abstract domain rather than running it.
link checked 17 Sept 2026Edmund M. Clarke & E. Allen Emerson
Introduces branching-time temporal logic as a specification language for concurrent programs and an algorithm for checking a finite-state program against it automatically, founding model checking as a field.
Martín Abadi & Leslie Lamport
Gives conditions under which a lower-level specification correctly implements a higher-level one, formalising 'refinement' as a mapping between the two systems' state spaces that a verifier can check mechanically.
J.M. Spivey
Defines Z's set-theoretic and schema notation precisely enough to serve as its own standard, giving specifiers a mathematical language for describing what a system must do before anyone writes code.
Gerard J. Holzmann
Describes SPIN's design for verifying concurrent software by directly checking process interaction models against linear temporal logic properties, and reports its use finding real protocol bugs.
Dawson Engler, Benjamin Chelf, Andy Chou & Seth Hallem
Lets programmers write small, system-specific correctness rules as compiler extensions, and reports that checking Linux and other large codebases this way found hundreds of real bugs missed by generic analysis.
Leslie Lamport
Introduces TLA+ and argues that writing a precise specification of a concurrent system, before coding it, is what actually catches its bugs.
Assumes predicate logic and set theory, and a willingness to write the specification before the code
link checked 17 Sept 2026Anthony Hall & Roderick Chapman
Reports building a certified secure system by specifying and proving properties before writing code rather than testing them in afterwards, and argues the resulting defect rate justifies the extra upfront cost.