Formal verification
Proving or disproving that a system meets a formal specification, by mathematics rather than by testing. The Wikipedia survey splits the field into three techniques and the split is the useful part, because cluster E has been paging the tools without the map they sit on.
- Model checking — explore a mathematical model of the system exhaustively and check a property holds. Finite systems only, and symbolic methods run out at a few hundred bits of state. tla-plus is the corpus’s instance.
- Deductive verification — generate proof obligations and discharge them, with an interactive prover (isabelle, HOL, ACL2, and by extension lean-theorem-prover and rocq) or an automatic SMT solver. More work per system, but it scales past what model checking can enumerate.
- Abstract interpretation and type-based methods, with dependent types named as promising for software.
Verified artifacts it names: seL4, the microkernel proved correct (already on isabelle); CompCert, a formally verified C compiler covering most of ISO C (already on rocq); and Yale’s CertiKOS kernel, 2016. Hardware is where adoption is routine — most leading hardware companies verify, because designs are complex and mistakes are expensive. Software adoption lags.
T2 — an encyclopedia survey, secondary by construction, and the first source here that describes the field rather than one of its tools.
What it changes for cluster E
The spoke’s formal-methods cluster grew tool-first: Lean, Rocq, Isabelle, TLA+, alphaproof, lean-certificate. Reading them against this survey, two things land.
The tools were not all doing the same job. tla-plus is model checking a design; Isabelle proving seL4 is deductive verification of an implementation; Lean formalizing mathematics is deductive verification with no system underneath it at all. The corpus had been treating “formal methods” as one activity with several products. It is at least three, separated by what gets exhausted — states, proof obligations, or abstract domains.
The named limitations are the same three the cluster reached independently. State explosion caps model checking. Cost — human and computational — caps everything. And the specification problem: someone must write what correct means. lean-certificate arrived at that last one from the other direction, when the spoke concluded a certificate proves the theorem as stated and says nothing about whether the statement was the right one. A survey of the whole field names it as the field’s own standing difficulty, which upgrades that page’s finding from a local observation to the discipline’s known hole.
The hardware/software asymmetry is new here and worth keeping. The same mathematics is routine in chip design and rare in software. That is an economic fact about the cost of a recall versus a patch, not a technical one about the methods, and it explains where the corpus’s verified-software examples come from: kernels, compilers and avionics, where the patch is also expensive.
Cross-spoke
../programming-languages-wiki holds spark, the Ada subset built for deductive verification, where
this stops being a research programme and becomes a language a defence contractor ships. That page and
this one are the two ends of the same technique.
Related
tla-plus · isabelle · rocq · lean-theorem-prover · lean-certificate · alphaproof · synthesis