L'IA et Lean relancent la vérification formelle du code

L'IA fait entrer la vérification formelle dans une nouvelle dimension. Plus tôt dans l’année, le PDG de Google, Sundar Pichai, a indiqué qu’environ 75% du nouveau code de l’entreprise était produit par des modèles avant d’être relu par des ingénieurs, et Anthropic affirme que plus de 80% de son code interne est rédigé par Claude. Mais cette automatisation accroît les défauts: une étude de CodeRabbit sur 470 projets open source a constaté 1,7 fois plus de bugs dans les contributions assistées par IA. Face à une production plus rapide que la relecture humaine, l’industrie se tourne vers une méthode vieille d’un demi-siècle, consistant à prouver par des outils comme Lean, Rocq ou Isabelle qu’un programme respecte toujours une règle. Historiquement coûteuse, la vérification formelle exige de traduire le comportement attendu en logique puis de produire des démonstrations vérifiées par ordinateur. Le micro-noyau seL4, projet emblématique, a demandé environ 20 personnes-années. L’IA change l’équation: un assistant de preuve accepte ou refuse la démonstration, ce qui contraint le modèle à répéter ses essais sans pouvoir tricher. En août, une étude de Stanford a montré que l’IA pouvait compléter en 11,4 heures, pour environ 467 dollars, une tâche de vérification de bibliothèques cryptographiques ayant mobilisé des humains pendant huit mois. Le mouvement s’accélère avec des acteurs majeurs. Le 26 octobre, Axiom Math a annoncé avoir formalisé en 24 jours une démonstration mathématique géante, produisant plus de 43 millions de lignes de code pour Lean. Le projet a aussi révélé 34 erreurs dans des démonstrations publiées, dont certaines persistaient depuis près de quarante ans. Anthropic et Theorem ont utilisé Claude sur des dizaines de bibliothèques open source, générant environ 180 millions de lignes de preuves et corrigeant des centaines de failles. Depuis le 27 octobre, Harmonic applique son prouveur Aristotle, remarqué en mathématiques, à des programmes C et à des puces, avec des résultats déjà notés par l’entreprise de puces Tensordyne. Le capital suit: Axiom, Harmonic, &Truth et Pramaana Labs totalisent plus de 650 millions de dollars levés. Ces projets répondent à un enjeu critique, vérifier des logiciels et des décisions dans des secteurs exposés. &Truth, sortie de confidentialité le 29 octobre avec 70 millions de dollars de financement, vise une machine capable de comprendre plusieurs langages de programmation à partir de Lean, en promettant des gains de vitesse considérables. Pramaana Labs, de son côté, convertit des règles fiscales, juridiques ou médicales en références vérifiables pour contrôler les réponses de l’IA. Même si des dirigeants de la sécurité restent sceptiques, plusieurs sociétés spécialisées constatent une demande supérieure à leur capacité. Les limites restent néanmoins majeures. La méthode prouve la conformité à une spécification, pas l’exactitude de cette spécification. Si l’IA écrit à la fois le code, la règle et la preuve, sans supervision indépendante, la garantie peut se transformer en boucle autoréférencée. La force de la vérification formelle tient pourtant à une promesse plus robuste: des résultats mathématiques peuvent être réexaminés par tous. Dans un paysage où les modèles génèrent et attaquent les logiciels, la question déterminante sera donc de savoir qui définit les standards et qui les contrôle, pour éviter que la preuve ne devienne un simple label commercial.