L’essentiel
- Mistral publie Leanstral 1.5, un modèle ouvert (licence Apache 2.0) dédié à la vérification formelle dans le langage Lean 4.
- Lors d’un test grandeur nature, il a passé au crible 57 dépôts open source et repéré cinq bugs jusque-là inconnus, dont un dépassement d’entier dans la bibliothèque Rust varinteger.
- Sur le benchmark de maths formelles miniF2F il atteint 100 %, et résout 587 des 672 problèmes de PutnamBench.
Une intelligence artificielle peut-elle vous garantir qu’un programme ne se trompera jamais ? Pas « probablement », pas « à 99 % » : la certitude, au sens mathématique du terme. C’est la promesse un peu vertigineuse de la vérification formelle, longtemps confinée à une poignée de laboratoires. Mistral vient de sortir un modèle libre taillé pour ça, et le résultat le plus parlant ne tient pas dans un score de concours.
Un langage conçu pour démontrer
Leanstral 1.5 est entraîné pour écrire du Lean 4, un langage de programmation dont la vocation n’est pas de faire tourner une application, mais de démontrer qu’un énoncé est vrai : un théorème de maths, ou la correction d’un morceau de code. Chaque affirmation doit être justifiée, ligne à ligne, jusqu’à ce qu’il ne reste aucune zone d’ombre. Si la preuve passe, c’est prouvé. Point.
Prenez la différence entre un correcteur orthographique, qui suggère une réponse plausible, et un huissier, qui constate un fait vérifiable. La plupart des assistants de programmation que vous connaissez appartiennent à la première famille : ils produisent du code vraisemblable, parfois faux avec aplomb. Un outil de preuve appartient à la seconde. Il ne propose pas, il établit.
Côté performance brute, les chiffres avancés par Mistral sont solides. Le modèle atteint 100 % sur miniF2F, un banc d’essai qui va du niveau lycée jusqu’aux problèmes d’olympiades. Sur PutnamBench, tiré du redoutable concours Putnam, il résout 587 des 672 énoncés, là où la précédente référence ouverte, le prouveur DeepSeek, n’en résolvait qu’une cinquantaine. Sur les tests d’algèbre avancée FATE-H et FATE-X, il domine le classement des modèles ouverts. Seul l’Aleph Prover, resté fermé, le devance sur l’un des tableaux. De quoi soigner la vitrine. Mais le plus révélateur s’est joué hors des concours.
Des théorèmes à la chasse aux bugs
Leanstral a beau avoir été entraîné surtout pour les mathématiques, Mistral l’a lâché sur du vrai code. L’éditeur raconte lui avoir fait analyser 57 dépôts open source. Verdict : cinq bugs jusqu’alors inconnus, dont un dépassement d’entier (overflow) dans varinteger, une bibliothèque écrite en Rust.
Un dépassement d’entier, c’est ce qui arrive quand un nombre grossit au-delà de la capacité prévue pour le stocker et « repasse » brutalement à une valeur aberrante, souvent négative. Le genre de faille discrète qui ne se déclenche que dans un cas limite, échappe aux tests classiques, et fait un jour planter un système en production. Débusquer ce type de défaut à la lecture, sans même exécuter le programme, c’est précisément ce que la vérification formelle sait faire et que les autres approches ratent.
Un modèle vendu pour ses talents de mathématicien devient ainsi, presque en passant, un traqueur d’erreurs que les développeurs n’avaient pas vues. Cinq trouvailles sur 57 dépôts, ce n’est pas un audit industriel, mais c’est une démonstration de faisabilité qui parle à quiconque a déjà chassé un bug fantôme un vendredi soir.
L’écart avec les assistants probabilistes
Pour saisir la portée de la chose, il faut regarder ce qui domine aujourd’hui le développement assisté. Les grands modèles de langage grand public génèrent du code par prédiction : ils devinent la suite la plus probable, en s’appuyant sur des milliards d’exemples. Génial pour aller vite, mais leur confiance n’est pas une garantie. Un assistant peut vous livrer une fonction élégante, parfaitement lisible, et fausse.
Leanstral change la nature de la promesse. Là où un assistant classique dit « voici sans doute la bonne réponse », un moteur de preuve dit « voici une réponse dont voici la démonstration, vérifiable par une machine ». La nuance n’est pas cosmétique : elle sépare la plausibilité de la certitude. Sur du code critique, ce déplacement compte plus que dix points de benchmark.
Et le fait que Mistral publie tout ça sous licence Apache 2.0, accessible via Hugging Face et une API gratuite, n’est pas un détail. La vérification formelle restait un savoir-faire de spécialistes, freiné par sa courbe d’apprentissage. Mettre un modèle capable de générer ces preuves à disposition de tous, c’est baisser la barrière d’entrée d’un domaine réputé aride.
Encore faut-il décrire ce qu’on attend du programme
Restons lucides. Le modèle a été entraîné d’abord pour les maths ; la vérification de code reste, pour l’instant, une capacité de bord, pas sa raison d’être. Cinq bugs relevés lors d’un test maison ne valent pas un déploiement à grande échelle sur des millions de lignes. Surtout, la vérification formelle exige que le comportement attendu soit spécifié rigoureusement en amont, un travail que peu d’équipes font aujourd’hui. Un moteur de preuve ne devine pas ce que votre programme est censé faire : il vérifie qu’il fait ce que vous avez formellement décrit.
Autrement dit, l’outil est puissant là où on prend la peine de formuler la question avec la précision d’un mathématicien. C’est encore rare dans l’industrie. Mais entre l’état de l’art d’hier, réservé aux thèses et aux systèmes ultra-sensibles, et un modèle ouvert qui trouve seul des failles réelles, la distance vient de se réduire d’un coup.
Mon avis
Les trois prochaines années vont sortir la preuve formelle du labo pour l’installer dans les chaînes d’intégration continue du code sensible : finance, aérospatial, cryptographie. Tant qu’elle réclamait des experts rares, elle restait un luxe. Un modèle ouvert qui déniche cinq bugs inédits sans qu’on le lui demande vraiment, ça déplace la ligne. Je ne mise pas sur la fin des assistants probabilistes, mais sur leur mariage avec ces moteurs de preuve : l’un propose vite, l’autre certifie. C’est ce couple-là qui rendra enfin fiable le code écrit par des IA.
