formal verification
In plain wordsUsing mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way.
Establishing by mathematical proof, rather than by testing, that a hardware design, program, protocol or learned model meets a formal specification for every possible input or execution — or finding a counterexample showing that it does not. The main techniques are model checking, which exhaustively explores a system's states for violations of properties stated in temporal logic; deductive verification, which proves programs correct against pre- and postconditions with proof assistants or SMTsatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met.-backed verifiers; and abstract interpretation, which soundly over-approximates program behavior. Industrial uses include processor and protocol design, aerospace and railway software, operating-system kernels such as seL4, and cloud access-control policies. In AI, verifiers certify properties of neural networksneural network, n.: A kind of computer program that learns a task from examples by tuning thousands to billions of connections between simple number-crunching units, an arrangement loosely inspired by nerve cells in the brain., such as robustness to small input perturbations, though only for modest-sized networks and narrow properties; and language modelslarge language model, n.: A computer program trained on enormous amounts of text to predict the words that come next. At vast scale, that simple skill lets it chat, answer questions, translate, summarize and write code. increasingly generate code together with machine-checkable proofs, which some researchers propose as a foundation for provably safe AI.
Formal verification proved the scheduler deadlock-free for every interleaving, something no amount of testing could show.
Origin
Grew from program-correctness work by Robert Floyd (1967) and Tony Hoare (1969). Edmund Clarke and E. Allen Emerson, and independently Jean-Pierre Queille and Joseph Sifakis, introduced model checking in 1981–1982, earning Clarke, Emerson and Sifakis the 2007 Turing Award; neural-network verification grew rapidly after the Reluplex solver (2017).
Usage note
A verified system is only as trustworthy as its specification and its model of the environment: a proof says nothing about properties that were never stated. Not to be confused with a verifierverifier, n.: A program or AI model that checks whether a proposed answer is correct — by running tests, comparing with a known result or judging the reasoning — so that good answers can be picked or rewarded. in language-model training, which is usually a learned or programmatic checker of answers.
Related
- satisfiability modulo theoriessatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met.
- interactive theorem provinginteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs.
- autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify.
- adversarial exampleadversarial example, n.: An input altered on purpose, often too slightly for people to notice, so that an AI model gets it badly wrong — like a panda photo that a classifier confidently calls a gibbon.
- verifierverifier, n.: A program or AI model that checks whether a proposed answer is correct — by running tests, comparing with a known result or judging the reasoning — so that good answers can be picked or rewarded.
Sources
- Hoare, C. A. R. (1969). An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–580.
- Katz, G., Barrett, C., Dill, D. L., Julian, K. & Kochenderfer, M. J. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV 2017, LNCS 10426.
Mentioned in
combinatorial explosioncombinatorial explosion, n.: The way the number of possible combinations — moves, routes, schedules — grows so quickly as a problem gets bigger that checking them all becomes impossible, even for the fastest computers., Gödel's incompleteness theoremsGödel's incompleteness theorems, n.: Two famous results from 1931 showing that any consistent set of rules for doing arithmetic leaves some true statements unprovable, and cannot prove that it is itself free of contradictions., interactive theorem provinginteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong., autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify., branch and boundbranch and bound, n.: A method for finding the provably best answer to a hard puzzle: divide the possibilities into groups, quickly estimate the best any group could offer, and throw out every group that cannot beat the best answer already in hand., guaranteed safe AIguaranteed safe AI, n.: A proposed approach to AI safety in which systems come with mathematical proofs or checkable guarantees that they will not cause certain harms, instead of relying on testing alone., IsabelleIsabelle, prop. n.: A widely used proof-checking program in which people write mathematics and verified software; it is known for automation that calls other theorem provers to finish routine steps., RocqRocq, prop. n.: A long-established computer system, known until 2025 as Coq, in which people write mathematical proofs and verified software that the computer checks step by step., satisfiability modulo theoriessatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met., temporal logictemporal logic, n.: A logic for statements about time — 'eventually the light turns green', 'the door is never open while the train moves' — used to specify and check how systems must behave over time.