Lawrence C Paulson ouvre sa chronique en rejetant la thèse, défendue par Peter Thiel et divers influenceurs YouTube, selon laquelle la science stagne depuis 50 ans. Son contre-exemple est son propre domaine : les assistants de preuve de style LCF.

L'histoire commence en 1975 avec Edinburgh LCF, le système de Robin Milner présenté à la conférence d'Arc-et-Senans. Il a établi le schéma toujours en vigueur : un noyau de preuve encapsulé dans un type abstrait en ML, de sorte que seules les règles d'inférence peuvent produire des valeurs de type thm. S'y ajoutaient des règles de déduction naturelle, la preuve dirigée par le but avec tactiques et combinateurs de tactiques, et des théories structurées. La logique était minimale : quantification universelle, conjonction et implication, sans nombres négatifs ni notation décimale. Paulson a rejoint Milner et Mike Gordon à Cambridge en 1982, a profondément remanié le système en Cambridge LCF et a vérifié l'algorithme d'unification en 36 inductions.

De 1985 à 1995, le compilateur ML plus rapide de Cambridge LCF a alimenté HOL88 de Gordon, et la vérification matérielle est devenue réalité : des conceptions de puces de production ont été vérifiées pendant que la vérification logicielle stagnait. Le développement d'Isabelle a commencé en 1986, écrit en Standard ML dès le départ. Le calcul des constructions inductives est apparu, le formalisme derrière les systèmes actuels Rocq et Lean. Isabelle/HOL est sorti pour la première fois en 1991, principalement l'œuvre de Tobias Nipkow.

Le bug FDIV du Pentium en 1994, dont le rappel a coûté près d'un demi-milliard de dollars à Intel, a poussé John Harrison vers la vérification de l'arithmétique flottante. Sa thèse de 1996 a formalisé l'analyse réelle dans HOL : espaces métriques, limites, différentiation, intégration et preuves flottantes selon la norme IEEE. L'automatisation a progressé avec le prouveur Metis de Hurd et le simplificateur d'Isabelle. Proof General a offert à plusieurs systèmes une interface Emacs commune.

En 2005, le domaine comptait des résultats marquants : la preuve Coq du théorème des quatre couleurs par Gonthier, la formalisation du théorème des nombres premiers par Avigad dans Isabelle, et la vérification du processeur ARM6 par Gordon, Birtwistle et Fox. Isabelle a gagné le langage de preuve Isar, les classes de types, des chercheurs de contre-exemples et la génération de code.

La décennie suivante a apporté seL4, le premier noyau de système d'exploitation formellement vérifié, aujourd'hui soutenu par un million de lignes de preuves Isabelle/HOL. CompCert a livré un compilateur vérifié pour un large sous-ensemble de C, et CakeML a bouclé le cercle du bootstrap avec un compilateur vérifié jusqu'à l'assembleur. En mathématiques ont suivi le second théorème d'incomplétude de Gödel, le théorème central limite, le projet Flyspeck et le théorème de l'ordre impair.

La dernière décennie a conquis les mathématiques grand public, portée par la promotion de Lean par Kevin Buzzard. En 2022, l'assistance machine a confirmé pour la première fois des mathématiques nouvelles qu'un médaillé Fields avait mises en doute. Dans l'industrie, Isabelle a contribué à l'architecture à capacités CHERI et à la spécification WebAssembly, où Conrad Watt a trouvé des problèmes corrigés à temps. Le 4 décembre 2025, AWS a annoncé le Nitro Isolation Engine pour Graviton5 : un noyau de séparation écrit en Rust avec 260 000 lignes de preuves Isabelle/HOL couvrant confidentialité et intégrité, un projet auquel Paulson participe lui-même.

Sa comparaison finale : les smartphones étaient autrefois révolutionnaires et n'attirent plus de foules. La vérification formelle n'est pas encore banale, mais elle s'en rapproche.