L'IA sait écrire du code depuis deux ans. Mais qui prouve que ce code est correct ? Le 2 juillet 2026, Mistral AI a apporté une réponse inattendue avec Leanstral 1.5 : un modèle open source sous licence Apache 2.0, spécialisé non pas dans la génération de code, mais dans sa vérification formelle. Autrement dit : la démonstration mathématique qu'un programme fait exactement ce qu'il est censé faire. Et ce n'est pas de la théorie — le modèle a déjà déniché cinq bugs inconnus dans des projets open source réels.
Un modèle qui ne code pas, il démontre
Leanstral 1.5 est construit pour Lean 4, l'assistant de preuve utilisé par les mathématiciens et, de plus en plus, par les ingénieurs qui veulent vérifier formellement leurs logiciels. Le principe : au lieu de tester un programme sur quelques cas et d'espérer que le reste tienne, on écrit une preuve mathématique que la propriété voulue est vraie pour toutes les entrées possibles.
Jusqu'ici, cette rigueur était réservée à une élite : l'aéronautique, le ferroviaire, le nucléaire, quelques équipes de cryptographie. Écrire des preuves formelles coûte un temps considérable et exige des compétences rares. C'est exactement ce verrou que Mistral attaque, avec un slogan assumé : « Proof Abundance for All » — la preuve pour tous.
Sous le capot, l'architecture est astucieuse : un Mixture of Experts de 119 milliards de paramètres, dont seulement 6,5 milliards activés à chaque inférence (128 experts, 4 actifs par token). Résultat : une intelligence de grande taille au coût d'exécution d'un petit modèle. L'entraînement combine mid-training, fine-tuning supervisé et apprentissage par renforcement via la méthode CISPO.
Des benchmarks littéralement saturés
Les chiffres publiés par Mistral sont spectaculaires. Le modèle sature miniF2F, le benchmark historique de preuve formelle, désormais trop facile pour lui. Sur PutnamBench — des problèmes issus de la compétition mathématique universitaire la plus exigeante des États-Unis — il résout 587 problèmes sur 672.
Sur les benchmarks FATE, conçus pour évaluer la vérification formelle appliquée, Leanstral 1.5 atteint 87 % sur FATE-H et 34 % sur FATE-X, deux scores état de l'art. Pour situer : FATE-X est calibré pour résister aux meilleurs modèles du marché, tous éditeurs confondus.
Mais les benchmarks ne sont que la vitrine. Le vrai test, c'est le monde réel.
Cinq bugs que personne n'avait vus
Mistral a lâché son modèle sur 57 dépôts open source en mode agent : lire le code, formuler des propriétés à vérifier, tenter de les prouver. Quand la preuve échoue, deux possibilités — soit la preuve est mal engagée, soit le code est faux.
Bilan : cinq bugs jusqu'alors inconnus, découverts par l'échec de preuves. L'exemple le plus parlant vient de la bibliothèque datrs/varinteger : dans la fonction de décodage zigzag, l'expression (value + 1) provoque un dépassement d'entier sur la valeur maximale U64. Conséquence : crash en mode debug, corruption silencieuse de données en mode release. Le genre de bug qu'aucune suite de tests classique n'attrape, parce que personne ne pense à tester la valeur limite exacte.
C'est toute la différence entre tester et prouver. Un test vérifie des exemples. Une preuve couvre l'infini des cas — y compris celui auquel vous n'avez pas pensé.
Pourquoi c'est un tournant pour le code généré par IA
Le timing n'a rien d'un hasard. En 2026, une part massive du code en production est écrite par des assistants IA — Claude Code, Cursor, Copilot et consorts. La productivité a explosé, mais une question dérange : qui relit vraiment ce code ? Les études s'accumulent sur les vulnérabilités et régressions introduites par du code généré puis validé trop vite.
La réponse de l'industrie jusqu'ici : encore plus de tests, encore plus de revue par IA. Mistral propose un chemin différent : faire vérifier le code généré par une machine dont le verdict est mathématiquement irréfutable. Un agent qui écrit le code, un autre qui prouve sa correction — la boucle devient vertueuse, et surtout auditable.
Le choix de l'open source change aussi la donne. Poids ouverts sur Hugging Face, licence Apache 2.0, API gratuite : là où la vérification formelle était un service de niche hors de prix, elle devient un outil qu'une équipe peut auto-héberger, y compris sur du code confidentiel qui ne doit jamais sortir de l'entreprise. Face aux géants américains qui verrouillent leurs modèles de raisonnement, l'Européen joue la carte de l'ouverture — et sur ce créneau précis, il est aujourd'hui devant.
Mon analyse : la fin du « ça a l'air de marcher »
Je vois dans Leanstral 1.5 un signal plus important que la plupart des annonces de modèles génériques de ce début d'été. Pas parce que tout le monde va écrire des preuves Lean 4 demain matin — soyons honnêtes, la marche reste haute pour une équipe web classique.
Mais une direction se dessine : demain, les morceaux critiques d'un logiciel — calculs financiers, gestion des droits, parsing de données, chiffrement — pourront être prouvés corrects automatiquement, pendant que le reste continue de vivre avec des tests classiques. Les outils de développement IA intégreront cette brique comme ils ont intégré le linting : silencieusement, en tâche de fond.
Pour les décideurs techniques, le message est concret : la question « peut-on faire confiance au code généré par l'IA ? » est en train de changer de réponse. Hier, c'était « faites-le relire ». Demain, ce sera « exigez la preuve ». Et le fait que cette brique soit open source, européenne et gratuite devrait faire réfléchir tous ceux qui pensaient que la course à l'IA ne se jouait que sur la taille des modèles.
