Lawrence C Paulson eröffnet seine Chronik mit einer Abfuhr an Peter Thiel und diverse YouTube-Stimmen, die behaupten, die Wissenschaft stagniere seit 50 Jahren. Sein Gegenbeispiel ist sein eigenes Fachgebiet: Beweisassistenten im LCF-Stil.

Die Geschichte beginnt 1975 mit Edinburgh LCF, Robin Milners System, vorgestellt auf der Konferenz in Arc-et-Senans. Es etablierte das bis heute gültige Muster: einen Beweiskern, gekapselt in einem abstrakten Typ in ML, sodass nur Inferenzregeln Werte vom Typ thm erzeugen können. Dazu kamen Regeln im Stil des natürlichen Schließens, zielgerichtetes Beweisen mit Taktiken und Taktikalen sowie strukturierte Theorien. Die Logik war winzig: Allquantor, Konjunktion und Implikation, ohne negative Zahlen oder Dezimalschreibweise. Paulson stieß 1982 zu Milner und Mike Gordon in Cambridge, baute das System zu Cambridge LCF um und verifizierte den Unifikationsalgorithmus in 36 Induktionen.

Von 1985 bis 1995 floss der schnellere ML-Compiler von Cambridge LCF in Gordons HOL88 ein, und Hardware-Verifikation wurde Realität: Produktionsreife Chipdesigns wurden verifiziert, während Software-Verifikation hinterherhinkte. 1986 begann die Isabelle-Entwicklung, von Anfang an in Standard ML geschrieben. Der Kalkül der induktiven Konstruktionen entstand, der Formalismus hinter den heutigen Systemen Rocq und Lean. Isabelle/HOL erschien erstmals 1991, vor allem das Werk von Tobias Nipkow.

Der Pentium-FDIV-Bug von 1994, dessen Rückruf Intel fast eine halbe Milliarde Dollar kostete, brachte John Harrison zur Gleitkomma-Verifikation. Seine Dissertation von 1996 formalisierte reelle Analysis in HOL: metrische Räume, Grenzwerte, Differentiation, Integration und Gleitkomma-Beweise nach IEEE-Standard. Die Automatisierung legte zu, mit Hurds Metis-Beweiser und Isabelles Simplifier. Proof General gab mehreren Systemen eine gemeinsame Emacs-Oberfläche.

Bis 2005 gab es erste Meilensteine: Gonthiers Coq-Beweis des Vierfarben-Satzes, Avigads Formalisierung des Primzahlsatzes in Isabelle und die Verifikation des ARM6-Prozessors durch Gordon, Birtwistle und Fox. Isabelle erhielt die Beweissprache Isar, Typklassen, Gegenbeispielsucher und Codegenerierung.

Das Jahrzehnt nach 2005 brachte seL4, den ersten formal verifizierten Betriebssystemkernel, heute gestützt auf eine Million Zeilen Isabelle/HOL-Beweise. CompCert lieferte einen verifizierten Compiler für eine große C-Teilmenge, und CakeML schloss den Bootstrapping-Kreis mit einem verifizierten Compiler bis hinunter zur Assemblersprache. In der Mathematik folgten Gödels zweiter Unvollständigkeitssatz, der Zentrale Grenzwertsatz, das Flyspeck-Projekt und der Satz über Gruppen ungerader Ordnung.

Das letzte Jahrzehnt brach in die Mathematik ein, getrieben von Kevin Buzzards Werbung für Lean. 2022 bestätigte maschinelle Unterstützung erstmals neue Mathematik, an der ein Fields-Medaillenträger gezweifelt hatte. In der Industrie steuerte Isabelle zur CHERI-Capability-Architektur und zur WebAssembly-Spezifikation bei, wo Conrad Watt rechtzeitig Fehler fand. Am 4. Dezember 2025 kündigte AWS die Nitro Isolation Engine für Graviton5 an: einen in Rust geschriebenen Trennkernel mit 260.000 Zeilen Isabelle/HOL-Beweisen zu Vertraulichkeit und Integrität, ein Projekt, an dem Paulson selbst mitarbeitet.

Seine Schlussbemerkung: Smartphones galten einst als Revolution und locken heute keine Schlangen mehr an. Formale Verifikation ist noch nicht alltäglich, aber sie ist auf dem Weg dorthin.