Leanstral : l’agent open source pour l’ingénierie de code fiable et des preuves formelles

• Premier agent de code open source conçu pour Lean 4, avec pour objectif d’automatiser les preuves formelles (formal proof) afin de réduire la charge de vérification humaine
• Les poids du modèle sont publiés sous licence Apache 2.0, et l’outil est immédiatement utilisable via l’environnement Mistral Vibe et un endpoint API gratuit
• Il s’appuie sur une architecture sparse de 6B paramètres actifs pour améliorer l’efficacité et réduire les coûts, tout en prenant en charge les intégrations MCP comme lean-lsp-mcp
• Sur le benchmark FLTEval, il obtient de meilleurs scores que de grands modèles open source comme Qwen3.5, GLM5 et Kimi-K2.5, avec des performances comparables à Claude Sonnet pour un coût plus de 15 fois inférieur
• Cette nouvelle approche combine automatisation des preuves formelles et amélioration de la fiabilité du code, avec un potentiel d’usage aussi bien en mathématiques de recherche que pour le développement de logiciels critiques

---

Présentation de Leanstral

• Leanstral est le premier agent de code open source pour Lean 4, fonctionnant dans un environnement d’assistant de preuve (proof assistant)
  • Lean 4 permet de représenter des objets mathématiques complexes (par ex. les espaces perfectoids) ainsi que des spécifications logicielles
  • Contrairement aux systèmes de preuve existants, souvent centrés sur des wrappers de modèles génériques ou sur des problèmes isolés, Leanstral a été entraîné pour fonctionner efficacement sur des dépôts formels réalistes (formal repositories)
• Il adopte une architecture sparse avec 6B paramètres actifs, combinant inférence parallèle (parallel inference) et capacités de vérification de Lean
• La prise en charge des intégrations MCP le rend compatible avec des protocoles courants comme lean-lsp-mcp

Publication et accessibilité

• Les poids du modèle sont publiés sous licence Apache 2.0, et l’agent est proposé en mode agent dans Mistral Vibe
• Tout le monde peut y accéder via l’endpoint API gratuit (labs-leanstral-2603), et les retours utilisateurs serviront à améliorer les prochains modèles
• Un rapport technique et l’outil d’évaluation FLTEval sont publiés en parallèle afin de mesurer les performances réelles en ingénierie des preuves, au-delà des évaluations existantes centrées sur les mathématiques

Évaluation des performances

• L’évaluation se fonde sur la capacité à finaliser, au niveau des Pull Requests du projet FLT, l’ensemble des preuves formelles ainsi que la définition de nouveaux concepts mathématiques
• Modèles comparés : Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B

Leanstral vs. modèles open source

• Leanstral-120B-A6B atteint 26,3 points (pass@2), devant GLM5 (16,6 points) et Kimi-K2.5 (20,1 points)
• Alors que Qwen3.5 obtient 25,4 points en 4 exécutions (pass@4), Leanstral fait mieux avec deux fois moins d’exécutions
• À coût équivalent, les performances montent linéairement jusqu’à 29,3 points (pass@4)

Leanstral vs. gamme Claude

• Il affiche une avance de 2,6 points sur Sonnet (26,3 points vs 23,7 points), pour un coût d’exécution de 36 $ vs 549 $, soit plus de 15 fois moins cher
• En pass@16, il atteint 31,9 points, soit 8 points de plus que Sonnet
• Le meilleur score revient à Claude Opus 4.6 avec 39,6 points, mais pour un coût de 1 650 $, soit 92 fois celui de Leanstral
• Tous les benchmarks ont été exécutés dans l’environnement Mistral Vibe sans modification

Modèle	Coût ($)	Score
Haiku	184	23.0
Sonnet	549	23.7
Opus	1,650	39.6
Leanstral	18	21.9
Leanstral pass@2	36	26.3
Leanstral pass@4	72	29.3
Leanstral pass@8	145	31.0
Leanstral pass@16	290	31.9

Études de cas

Adaptation aux changements de version de Lean

• Entrée d’une question StackExchange portant sur une erreur liée à un alias de type apparue dans Lean 4.29.0-rc6
• Leanstral a reproduit l’environnement du problème et diagnostiqué avec précision un problème d’égalité définitionnelle (definitional equality)
• Il a proposé d’utiliser abbrev à la place de def, rétablissant ainsi le bon fonctionnement de la tactique rw
• Il a aussi expliqué clairement à l’utilisateur la cause du problème et la raison de la solution

Raisonnement sur les programmes et traduction

• Conversion d’une définition de programme en Rocq vers Lean, avec implémentation d’une notation personnalisée
• Exemple : démontrer que la commande plus2 ajoute bien 2 à la variable X
• À partir de la seule spécification Rocq fournie, Leanstral a complété et prouvé le théorème (theorem) dans Lean

Utilisation

• Intégration Mistral Vibe : disponible immédiatement avec la commande /leanstall
• Labs API : accès gratuit ou à faible coût
• Téléchargement du modèle : exécutable directement sous licence Apache 2.0

Portée

• Leanstral constitue la première tentative open source de combiner génération de code et automatisation des preuves formelles
• Il ouvre des perspectives d’usage en mathématiques de recherche, développement logiciel vérifiable et conception de systèmes à haute fiabilité
• Il est présenté comme une nouvelle infrastructure de vérification de code alliant efficacité économique et ouverture

[GN⁺]

Avis sur Hacker News

• Il est intéressant de voir que les gens commencent à reconnaître un schéma où l’on peut désormais spécifier à un agent le comportement souhaité, puis lui faire écrire du code conforme à cette spécification
  Qu’on utilise le TDD, des outils de vérification ou autre, avec le temps ces suites de validation finissent par s’accumuler comme un dépôt de documentation exécutable montrant « comment cela doit fonctionner »
  Cette approche est bien plus puissante qu’une simple spécification en Markdown, car elle capture dans le code non pas l’intention mais le comportement détaillé
  Plus le logiciel devient complexe, plus la transmission orale du type « demande à Jim » atteint ses limites

  • J’ai l’impression que la différence n’est pas si grande. Le code n’est au fond qu’une autre forme d’expression de ce qu’on mettrait dans un fichier .md
    La finesse et le contexte se perdent quand on change de niveau de résolution
    Je suis d’accord avec le TDD ou le développement centré sur la vérification, mais les écrire en code n’est pas l’objectif final
    Il existe déjà des millions de lignes de tests, donc le plus réaliste est de faire évoluer à partir de cette base
  • Avec l’arrivée de l’IA, je pense qu’on peut enfin atteindre la réalité dont le TDD rêvait
  • Cette approche est intéressante, mais l’article de blog m’a semblé confus
    Je me demande quelle aide Lean apporte concrètement.
    Par exemple, est-ce qu’on prouve une machine à états en Lean puis on la transpose en Dart ?
    Je connais mal Lean, donc j’ai du mal à voir si c’est une approche réaliste

• Comme cela a aussi été évoqué récemment dans le podcast de Jack Clark (cofondateur d’Anthropic) et Ezra Klein, il y a beaucoup de discussions sur le fait que l’alignement des modèles (alignment) est relatif et que la diversité est importante
  Certains estiment que le modèle de Mistral est en retard par rapport aux autres modèles de pointe, mais expérimenter différentes techniques d’alignement et différentes entreprises reste important pour l’écosystème

  • Au final, je pense que le temps réglera la question

• Ce cas de réussite concret rappelle le Red Green TDD de Simon Willison
  J’ai trouvé impressionnant le processus par lequel Leanstral a produit du code de test pour reproduire un environnement d’échec, puis a identifié un problème de définitional equality

  • Si l’agent écrit lui-même les tests, est-ce que cela garantit une meilleure exactitude que lorsque code et tests sont écrits séparément ?
  • Au fond, le TDD ressemble à du prompt engineering : c’est le processus qui consiste à donner un objectif clair à l’agent

• Ce modèle a été entraîné pour une tâche spécifique, mais ses performances restent inférieures à Opus
  Opus coûte six fois plus cher, mais cela semble en valoir la peine

  • L’idée est bonne, mais au final la qualité passe avant la fiabilité
    On comprend qu’une startup européenne peu capitalisée vise ce type de niche, mais cela semble difficile d’en faire un gros relais de revenus
  • La fiabilité des benchmarks reste floue, mais quand on regarde les résultats pass@2 ou pass@3, l’impression change
    Ce serait plus intéressant de comparer avec des modèles comme Codex
  • Le modèle est open source, donc on peut l’exécuter en local. Ce n’est pas un point assez important ?

• J’aime bien le concept de code fiable
  Mais le point de comparaison me paraît confus. On insiste sur le fait que c’est moins cher que Haiku, alors que Haiku est lui-même faible sur cette tâche et que Leanstral l’est encore davantage
  Si l’exactitude est l’objectif, je ne vois pas pourquoi « moins cher mais médiocre » serait important
  Cela dit, Opus n’est pas parfait non plus, donc avec un passage à l’échelle on pourrait peut-être obtenir de meilleurs résultats

  • Le graphique montre que les performances s’améliorent à mesure que le nombre de pass augmente
    À 2 essais, c’est meilleur que Haiku et Sonnet, et à 16 essais, cela se rapproche d’Opus tout en restant plus rentable
  • En fait, c’est simple — il suffit de demander dans le prompt « uniquement des sorties fiables »

• Ne connaissant pas Lean, je me demande si cela apporte une valeur directe
  Est-ce qu’on ajoute automatiquement des preuves à du code dans un langage comme Go, ou faut-il simplement soutenir la diversité des modèles ouverts ?

  • Ce doit sans doute être une architecture où l’agent génère une spécification Lean4, puis évalue le logiciel à partir de cette spécification
    Mais au final, la spécification Lean4 devient elle-même un artefact logiciel
    On retombe alors sur la question de vérifier si cette spécification est correcte — au bout du compte, il faut toujours une revue humaine

• J’anticipais cette tendance depuis quelques semaines, et je suis heureux de voir que cela se confirme
  À l’ère des LLM, il me semble que la convivialité du code pour les humains comptera moins que sa prouvabilité et son efficacité en tokens
  En combinant Lean et Rust, on pourrait peut-être arriver à un monde où « seul le code prouvé se compile »
  J’ai résumé des discussions liées dans un commentaire précédent

  • Cela dit, aucun système de preuve ne garantit qu’une preuve soit « juste »
    Il garantit seulement qu’elle est logiquement valide
    Comprendre pleinement ce que démontre une preuve est aussi difficile que comprendre un programme, même si cela a l’avantage d’approfondir la réflexion

• Je suis content de voir que le terme « open source » ne se limite pas ici aux mots, avec une publication réelle des weights sous licence Apache-2.0

  • Mais du point de vue des standards de la communauté, si le modèle n’est pas reproductible, ce n’est que de l’open weights, pas de l’open source

• Selon les actualités officielles de Mistral
  Claude Opus obtient un score de 39,6 pour un coût de 1 650 dollars,
  Leanstral pass@8 obtient 31,0 pour 145 dollars, et pass@16 31,9 pour 290 dollars,
  ce qui donne une très bonne efficacité coût/performance