L’automatisation des preuves Lean est arrivée. La partie difficile vient simplement de se déplacer

L’automatisation des preuves Lean a franchi un cap important le 26 juillet, lorsqu’Adam Langley a décrit l’utilisation de grands modèles de langage pour vérifier un décodeur Zstandard fonctionnel. Le résultat n’était ni un théorème de benchmark ni une démonstration soignée d’un fournisseur. Il s’agissait d’un projet logiciel ordinaire, avec des invariants difficiles, des preuves générées et un compilateur capable de rejeter les réponses erronées.

Cette combinaison change le débat habituel sur la fiabilité de l’IA. Un modèle de langage peut toujours halluciner, mal comprendre une exigence ou produire une syntaxe invalide. Pourtant, Lean vérifie la preuve obtenue au moyen d’un petit noyau de vérification : la confiance ne dépend donc pas du fait de croire le texte produit par le modèle.

Le véritable affrontement n’oppose donc pas le code généré par l’IA au code écrit par des humains. Il oppose la génération non vérifiée à la génération vérifiée par machine. Pour les travailleurs du savoir, cette distinction ouvre la voie à un modèle plus large dans lequel l’IA crée des artefacts tandis que des systèmes déterministes vérifient les affirmations importantes.

L’expérience de Langley ne démontre pas que la vérification formelle soit devenue bon marché, facile ou prête pour tous les systèmes de production. Il n’a pas publié le décodeur, et ses résultats en matière de performances étaient médiocres. Néanmoins, l’expérience offre un signal concret : l’économie de la vérification est en train d’évoluer.

Un décodeur Zstandard est devenu un test d’automatisation des preuves

L’expérience de Langley est importante parce que les LLM ont traité des obligations de preuve au sein d’une implémentation logicielle identifiable, et non uniquement des exercices mathématiques isolés.

Langley, ingénieur en sécurité reconnu pour ses travaux sur la cryptographie et les protocoles Internet, a construit un décompresseur Zstandard dans Lean. Lean est à la fois un langage de programmation fonctionnelle et un assistant de preuve interactif fondé sur la théorie des types dépendants.

Les types dépendants permettent aux types d’un programme d’exprimer des faits sur des valeurs particulières. Une fonction peut, par exemple, renvoyer un tableau dont le type indique sa longueur exacte. Une autre fonction peut exiger la preuve qu’un indice se trouve dans un tableau avant que Lean n’autorise l’accès.

Ces garanties peuvent encoder des hypothèses que les logiciels conventionnels laissent souvent dans des commentaires, des tests ou la mémoire d’un développeur. La référence officielle de Lean décrit un petit noyau qui vérifie les termes de preuve après leur génération par d’autres outils. Cette séparation entre génération et vérification est au cœur du sujet.

Langley a choisi Zstandard, souvent appelé zstd, comme cas de test. Zstd est un format de compression sans perte dont la complexité interne est suffisante pour rendre la vérification pertinente. Il utilise des correspondances de type LZ77 ainsi que le codage de Huffman et l’entropie à états finis, ou FSE.

La spécification de compression publiée pour ce format définit les trames, les blocs, les tables d’entropie, les codes de séquence et le comportement de décodage. Sa section consacrée à FSE décrit des tables d’états dont la construction doit préserver plusieurs relations pour les entrées possibles.

Une implémentation classique peut tester des tables sélectionnées par rapport à des sorties connues. La version Lean de Langley pouvait également énoncer des propriétés universelles de la fonction de construction de tables. Ces propriétés comprenaient la taille requise de la table, le nombre de symboles et la validité des transitions depuis les entrées de table.

C’est ici que la contribution des LLM est devenue significative. Selon le récit de Langley sur l’automatisation des preuves, plusieurs modèles ont produit les preuves pertinentes en environ 20 minutes. Il affirme que ce travail n’a consommé qu’une fraction de l’allocation d’un abonnement mensuel standard.

Les modèles n’ont pas laissé derrière eux la porte de sortie habituelle de Lean, appelée sorry, qui accepte une preuve inachevée durant le développement. Langley indique avoir confirmé que les preuves passaient la vérification de type et ne contenaient aucune lacune de ce type.

Cela ne valide pas indépendamment chaque affirmation concernant le décodeur. Langley n’a pas publié son code source ; des évaluateurs externes ne peuvent donc ni reproduire le projet ni examiner l’intégralité de sa spécification. Son rapport reste une expérience à la première personne plutôt qu’une évaluation par les pairs.

Pour autant, l’étape de vérification revendiquée n’a pas le même statut qu’une réponse ordinaire de chatbot. Si le noyau de Lean accepte une preuve pour un théorème correctement énoncé, le raisonnement privé du modèle n’a pas besoin d’être digne de confiance. Le vérificateur évalue l’objet formel obtenu.

C’est l’irrélevance des preuves sous une forme pratique. Pour de nombreuses propositions, le logiciel a finalement besoin d’une preuve valide, et non d’une explication élégante de la manière dont la preuve a été trouvée. Une preuve maladroite générée par machine peut tout de même certifier le théorème si le noyau l’accepte.

Le décodeur a également mis en évidence la frontière entre prouver un programme et construire un bon produit. Langley a rapporté que son implémentation était environ dix fois plus lente que l’implémentation zstd en ligne de commande. La vérification n’a pas automatiquement apporté des performances de production, de la maintenabilité ou une couverture complète du format.

Le résultat utile est plus circonscrit. Un développeur a utilisé des LLM généralistes pour satisfaire des obligations de preuve difficiles au sein d’un programme non trivial. L’expérience suggère que le travail de preuve, autrefois un coût dominant, peut de plus en plus devenir un travail généré par machine.

Pourquoi l’automatisation des preuves Lean modifie l’équation des coûts

L’automatisation des preuves Lean ne supprime pas les coûts de la vérification formelle, mais elle s’attaque à la catégorie de travail qui rendait ces coûts inacceptables pour les équipes logicielles ordinaires.

La vérification formelle offre depuis longtemps quelque chose que les tests ne peuvent pas fournir. Un test examine des exécutions sélectionnées, tandis qu’une preuve formelle peut établir une propriété énoncée pour tous les cas couverts par son modèle.

Cette distinction a produit des résultats remarquables dans les systèmes à haute assurance. Le micronoyau seL4 dispose de preuves vérifiées par machine reliant des spécifications à des implémentations vérifiées sur les configurations prises en charge. La documentation de son projet ne signale aucun défaut de correction fonctionnelle dans le code vérifié depuis l’achèvement de cette preuve en 2009.

Ces mêmes éléments de preuve sur seL4 illustrent aussi pourquoi les méthodes formelles sont restées spécialisées. Son effort de vérification a exigé des spécifications étendues, des scripts de preuve, des outils de support et du travail d’experts. Langley cite une estimation rétrospective selon laquelle le travail de preuve a demandé environ dix fois l’effort de conception et d’implémentation.

Il note également que le code de preuve dépassait l’implémentation C de plus de vingt fois. Les ratios exacts varient selon les projets et les objectifs de vérification. Le constat général reste clair : une assurance plus forte a historiquement exigé un vaste second corpus de travail technique.

Ce travail ne ressemble pas à la programmation conventionnelle. Les ingénieurs doivent traduire des exigences informelles en énoncés précis, décomposer des objectifs difficiles en lemmes gérables et guider les systèmes de preuve à travers les étapes manquantes. De petites modifications de code peuvent imposer des réparations de preuve considérables.

Les solveurs automatisés ont réduit une partie de cette charge. Des systèmes tels que F* peuvent envoyer des obligations adaptées à des solveurs modulo théories de satisfaisabilité, qui recherchent des preuves dans les théories logiques prises en charge. Toutefois, le comportement des solveurs peut devenir difficile à prévoir sur des objectifs complexes.

Les utilisateurs expérimentés apprennent souvent à formuler les définitions de façon à ce que l’automatisation réussisse. Cette expertise reste précieuse, mais elle déplace l’effort vers l’adaptation au solveur. Un petit choix de modélisation peut faire passer un résultat rapide à une recherche qui consomme beaucoup de temps.

Les LLM offrent une forme différente d’automatisation. Ils peuvent lire des définitions locales, interpréter les erreurs du compilateur, proposer des lemmes, réécrire du code et tenter une autre stratégie de preuve. Ils n’exigent pas que chaque obligation corresponde à une procédure de décision fixe.

La recherche montre déjà l’importance d’associer la génération à un vérificateur formel. Un système guidé par compilateur, décrit dans l’article APOLLO, utilise les retours de Lean pour réparer les preuves générées et isoler les sous-problèmes en échec. Ses résultats publiés montrent que la vérification itérative peut surpasser l’échantillonnage non guidé.

Le projet de Langley rapproche ce schéma de l’ingénierie logicielle quotidienne. Le modèle ne se contente pas de résoudre un théorème choisi pour un benchmark. Il rencontre des obligations de preuve créées par l’analyse d’octets, la construction de tables de décodage et l’application des limites de tableaux.

Cette différence compte pour l’adoption. La plupart des organisations n’emploient pas de mathématiciens pour prouver des problèmes de concours. Elles emploient en revanche des ingénieurs qui maintiennent des parseurs, des règles d’autorisation, des calculs financiers, de la logique de synchronisation et des transformations de données.

Ces systèmes contiennent d’innombrables énoncés que les équipes traitent déjà comme des invariants. Une requête appartient à un compte authentifié. Les lignes d’une facture correspondent à son total. Un parseur ne lit jamais au-delà de son tampon. Un flux de travail ne peut pas approuver sa propre action restreinte.

Les équipes protègent actuellement ces énoncés par des combinaisons de types, de tests, de revues, de surveillance et de contrôles opérationnels. Chaque méthode détecte des défaillances importantes, mais chacune laisse des lacunes. Les hypothèses dérivent également lorsque les exigences évoluent.

L’automatisation des preuves Lean offre une voie pour rendre certaines hypothèses exécutables et vérifiables. Le LLM absorbe une partie du travail de traduction et de preuve. Lean bloque ensuite les artefacts qui ne satisfont pas la spécification formelle.

Cet agencement modifie aussi le rôle de la confiance accordée à l’IA. Un assistant de codage conventionnel peut affirmer qu’un parseur est sûr après avoir examiné une fenêtre de contexte limitée. Un assistant qui produit des preuves doit fournir un artefact que Lean accepte face à une affirmation explicite.

Le modèle peut rester probabiliste parce que le seuil d’acceptation est déterministe. Cette architecture est plus importante que le score de benchmark d’un modèle particulier. De meilleurs modèles améliorent la vitesse et la couverture, tandis que le vérificateur préserve la frontière de confiance.

Pour les organisations, la question économique devient plus précise. Les équipes n’ont plus besoin de se demander si chaque ingénieur doit devenir expert en preuves. Elles peuvent se demander quelles défaillances coûteuses justifient des énoncés formels et des preuves assistées par l’IA.

Cette voie d’adoption plus étroite ressemble à la diffusion du typage statique, des tests automatisés et de l’intégration continue. Ces pratiques n’ont pas éliminé les défauts. Elles ont rendu certaines vérifications suffisamment peu coûteuses pour être exécutées durant le développement ordinaire plutôt que lors d’audits exceptionnels.

Le nouvel adversaire est la génération non vérifiée

Le conflit central ne consiste pas à déterminer si les humains ou les modèles écrivent un meilleur code. Il consiste à savoir si le travail généré est soumis à un test d’acceptation fiable.

La plupart des outils d’IA générative opèrent dans des domaines où la vérification est faible. Un modèle rédige un rapport, résume une réunion, propose une prévision ou modifie une politique. Le résultat paraît souvent plausible bien avant que quiconque sache s’il est correct.

La revue humaine reste la défense par défaut. Pourtant, les relecteurs font face à la même pression temporelle qui a motivé l’automatisation. Un brouillon fluide peut dissimuler une source manquante, une condition inversée ou une conclusion non étayée.

Les logiciels offrent davantage de retours automatisés que la plupart des activités de travail intellectuel. Les compilateurs rejettent les erreurs de syntaxe et de type. Les suites de tests exercent des cas connus. Les linters identifient certains motifs. La surveillance en production révèle les défaillances ayant franchi les contrôles précédents.

Aucun de ces mécanismes ne prouve habituellement une vaste affirmation sémantique. La réussite des tests ne peut pas établir que chaque flux compressé valide reste dans les limites des tableaux. Un vérificateur de types ne peut pas appliquer cette propriété, à moins que la relation pertinente n’apparaisse dans le système de types.

Lean modifie le contrat. Un développeur peut exprimer une affirmation dans les types du programme ou sous la forme d’un théorème. Le noyau vérifie ensuite si la preuve fournie établit cette affirmation exacte à partir des hypothèses acceptées.

Le LLM devient un producteur de preuves candidates plutôt qu’une autorité. Il peut échouer à répétition sans affaiblir la garantie finale. Une candidate défaillante est rejetée avant d’intégrer l’artefact de confiance.

Ce modèle devrait intéresser les travailleurs du savoir bien au-delà de la démonstration de théorèmes. De nombreux livrables professionnels contiennent déjà des affirmations vérifiables au regard de preuves structurées. Le défi consiste à distinguer ces affirmations des jugements qui restent contextuels.

Prenons le cas d’un chef de produit préparant un point hebdomadaire. Un assistant IA peut rassembler les notes de projet, décisions, retours clients et indicateurs de livraison via une base de connaissances consultable. Il peut rédiger un récit plus rapidement qu’une personne ne peut reconstituer la semaine.

Cependant, l’organisation a toujours besoin de garde-fous. Chaque déclaration de client citée doit renvoyer à un enregistrement ou à une note. Chaque fonctionnalité livrée doit renvoyer à un enregistrement de version validé. Chaque métrique doit indiquer sa définition et sa période de reporting.

Sous leur forme actuelle, il ne s’agit pas de tâches de démonstration de théorèmes. Elles partagent toutefois la même architecture. La génération propose un artefact, tandis qu’un système distinct vérifie les affirmations au regard de règles et de preuves explicites.

Un analyste financier pourrait exiger que chaque chiffre d’une note générée remonte à un dépôt réglementaire ou à un jeu de données approuvé. Un chercheur pourrait exiger que chaque citation étaye la phrase qui la contient. Une équipe conformité pourrait encoder les conditions de ses politiques dans des workflows vérifiables par machine.

Les langages formels relèvent le plafond de ces vérifications. Ils peuvent représenter des relations que de simples scripts de validation ne peuvent pas exprimer proprement. Les LLM aident alors les utilisateurs à rédiger des spécifications, relier des formats et construire les preuves requises.

Cela offre une définition plus utile d’une IA digne de confiance. La confiance ne vient pas du fait de demander à un modèle d’être prudent. Elle vient de la conception d’un processus dans lequel un travail non étayé ne peut franchir une frontière importante.

Cette approche précise également où le jugement humain demeure indispensable. Lean vérifie le théorème écrit par quelqu’un. Il ne détermine pas si ce théorème couvre le besoin réel de l’utilisateur ou l’ensemble des risques de l’organisation.

Une spécification parfaitement démontrée peut tout de même décrire le mauvais comportement. Un théorème sur les limites d’un tableau n’établit pas qu’un décodeur gère toutes les fonctionnalités requises par un service de production. Une preuve de sécurité peut omettre une capacité réaliste d’un attaquant.

Par conséquent, la vérification assistée par IA déplace l’effort humain vers la spécification. Les personnes doivent décider quelles propriétés comptent, quelles hypothèses sont acceptables et quelle frontière système couvre la preuve.

Ce déplacement ressemble à l’effet des tableurs sur la comptabilité. L’automatisation réduit le travail arithmétique, mais accroît l’importance du choix du bon modèle et des bonnes données d’entrée. Un calcul irréprochable peut néanmoins répondre à la mauvaise question métier.

Les équipes les plus solides ne traiteront pas les preuves générées comme des décorations. Elles examineront les énoncés de théorèmes, les hypothèses et les interfaces avec le même soin que celui aujourd’hui accordé à l’architecture et aux frontières de sécurité.

Ce que l’expérience Zstandard ne prouve pas

Une preuve vérifiée peut être valide alors que le logiciel environnant reste lent, incomplet, mal spécifié ou inadapté à la production.

La limite la plus immédiate est la reproductibilité. Langley n’a pas publié son implémentation, car il la considérait comme un projet d’apprentissage et non comme un décodeur de référence. Ce choix empêche toute évaluation indépendante du code, de la structure de la preuve et du workflow du modèle.

Les lecteurs devraient donc considérer le résultat rapporté de 20 minutes de génération de preuve comme un retour d’expérience. Il montre que le workflow a fonctionné pour un ingénieur expérimenté sur un projet. Ce n’est pas une mesure générale des performances.

Le modèle a également modifié du code d’implémentation pendant sa recherche de preuves. Langley avait utilisé Id.run, un mécanisme Lean permettant d’exprimer des calculs localement impératifs. Il indique que ce style rendait le code plus difficile à analyser pour les mécanismes de preuve.

Ce détail est plus révélateur qu’un simple récit de réussite. L’automatisation des preuves par IA ne s’est pas contentée de certifier une implémentation arbitraire. Elle a encouragé des changements rendant le programme plus facile à raisonner formellement.

De tels changements peuvent améliorer la structure, mais ils peuvent aussi déformer les priorités d’ingénierie. Les développeurs pourraient éviter des représentations efficaces parce que les outils de preuve actuels ont du mal à les traiter. Ils pourraient accepter un code plus lent afin d’obtenir une vérification plus rapide.

Le décodeur de Langley aurait fonctionné environ dix fois plus lentement que l’implémentation en ligne de commande établie. Cet écart n’invalide pas les preuves. Il montre que la correction, la couverture et les performances restent des dimensions distinctes.

L’ingénierie des preuves n’a pas disparu non plus. Les grands projets organisent les lemmes et les abstractions afin que les preuves résistent aux changements de code. Si un LLM peut régénérer les preuves à faible coût, certaines stratégies de maintenance deviennent moins importantes. D’autres restent nécessaires, car la recherche de preuves elle-même peut devenir coûteuse.

Des recherches récentes sur le snapshotting d’états de preuve illustrent ce problème d’infrastructure. Les auteurs indiquent que la reconstruction répétée des états peut dominer la recherche automatisée dans Lean. Leur mécanisme de réutilisation proposé a produit des accélérations substantielles sur certains benchmarks sélectionnés.

Cela rappelle que l’automatisation des preuves dépend de bien plus que de l’intelligence du modèle. Elle requiert un retour rapide du compilateur, une gestion des dépendances, la récupération des lemmes pertinents, une recherche contrôlée et des environnements reproductibles.

Le passage à l’échelle ajoute une autre incertitude. Un décodeur de compression possède une spécification contrainte et des algorithmes reconnaissables. Les systèmes d’entreprise mêlent bases de données, réseaux, interfaces utilisateur, services externes, permissions mutables et règles métier incomplètes.

La formalisation de ces frontières peut coûter plus cher que la démonstration de fonctions locales. Un théorème sur une règle d’autorisation n’est utile que lorsque les données d’identité, le comportement du service et la configuration de déploiement correspondent aux hypothèses du modèle.

Des types très expressifs peuvent également propager les changements dans un programme. Lorsqu’une structure de données acquiert un nouvel invariant, chaque fonction qui la construit ou la transforme doit satisfaire cette exigence renforcée. Cette propagation est précieuse, mais elle peut augmenter les coûts de migration.

Les LLM peuvent réparer les preuves affectées, mais ils ne peuvent pas toujours déduire l’intention produit à partir du code. Une preuve régénérée peut préserver l’énoncé d’hier alors que l’entreprise a en réalité besoin d’un nouvel énoncé. L’automatisation facilite le maintien d’une correction devenue obsolète.

La chaîne d’outils soulève aussi des enjeux de sécurité. Le noyau Lean réduit la base informatique de confiance, c’est-à-dire le logiciel qui doit se comporter correctement pour que la preuve soit digne de confiance. Cependant, des systèmes de build, parseurs, compilateurs et pipelines de déploiement entourent toujours ce noyau.

Les preuves reposent aussi sur des hypothèses et axiomes déclarés. Les équipes ont besoin de politiques rejetant les placeholders inachevés, les axiomes inattendus ou les preuves générées avec la mauvaise version de dépendance. Un simple indicateur vert dans l’éditeur ne constitue pas une gouvernance suffisante.

Le risque, pour les décideurs non techniques, est de surinterpréter le mot « preuve ». La vérification formelle établit une propriété définie sous des hypothèses définies. Elle ne certifie pas la qualité générale, le comportement éthique, l’utilisabilité, la conformité juridique ou la valeur métier.

Cette précision doit être considérée comme une force. Les équipes peuvent examiner exactement ce qui a été prouvé et ce qui est resté hors du périmètre. L’alternative consiste souvent en une vaste affirmation d’assurance étayée par des tests épars et une prose assurée.

Le résultat de Langley est donc surtout convaincant en tant que signal directionnel. Les LLM peuvent rendre la construction de preuves formelles moins exigeante en main-d’œuvre. Le goulot d’étranglement restant se déplace vers les spécifications, les frontières système, les performances et l’intégration.

Trois signaux montreront si l’automatisation des preuves se généralise

La prochaine phase dépend de cas logiciels reproductibles, d’outils de développement conscients des preuves et d’éléments montrant que les systèmes vérifiés restent maintenables après de véritables changements.

Le premier signal sera la publication de projets logiciels complets et ordinaires reposant sur des preuves Lean générées par IA. Les benchmarks restent utiles, mais ils ne capturent pas l’évolution des exigences, les mises à niveau de dépendances, l’optimisation des performances ou le débogage en production.

Un projet convaincant devrait exposer son code source, les énoncés de théorèmes, les prompts ou le workflow agentique, les versions des modèles, les commandes de vérification des preuves et ses limites. Des équipes indépendantes devraient pouvoir reproduire les preuves acceptées sans faire confiance à un modèle hébergé.

Si plusieurs projets apparaissent dans les parseurs, le code cryptographique, la logique financière et les implémentations de protocoles, la conclusion de Langley gagnera en force. Si les exemples restent petits ou non publiés, l’argument en faveur d’une adoption courante s’affaiblira.

Le deuxième signal sera l’intégration dans les workflows de développement grand public. L’automatisation des preuves doit ressembler moins à un environnement de recherche et davantage à la revue de code, à l’intégration continue ou au vérificateur de types d’un éditeur.

Les fonctionnalités importantes incluront une récupération fiable dans les bibliothèques locales, des boucles de retour courtes, des échecs explicables et une détection stricte des hypothèses inachevées. Les équipes auront aussi besoin d’artefacts de preuve versionnés, révisables à côté des changements de code.

Les outils devraient mettre en évidence les modifications de l’énoncé à prouver, et pas seulement du corps de la preuve. Un modèle qui affaiblit silencieusement un théorème peut transformer un échec difficile en réussite trompeuse. Les interfaces de revue doivent rendre cette manœuvre évidente.

Les organisations devraient également observer comment les fournisseurs relient les exigences informelles aux énoncés formels. Générer une preuve ne représente que la moitié du workflow. Le système doit préserver la traçabilité entre une décision humaine et une propriété vérifiée par machine.

C’est là que la gestion des connaissances devient une infrastructure opérationnelle. Les exigences, décisions, exceptions et preuves sources nécessitent un contexte durable avant qu’un assistant puisse les formaliser de manière responsable. Un système de connaissances personnel peut soutenir ce contexte, bien que l’acceptation formelle requière toujours des outils de vérification dédiés.

Le troisième signal sera le coût de maintenance après un changement substantiel. Une preuve unique peut impressionner les réviseurs tout en devenant un fardeau lors de la prochaine version. La mesure la plus pertinente est la vitesse à laquelle une équipe restaure un statut vérifié après avoir modifié un comportement.

Les chercheurs et les équipes d’ingénierie devraient publier des évaluations orientées changement. Ils devraient modifier des structures de données, renforcer des spécifications, remplacer des algorithmes et mettre à niveau des dépendances. Ils devraient ensuite mesurer l’effort humain, les tentatives du modèle, le temps de vérification et les régressions de performances.

Si l’IA peut réparer les preuves tout en préservant des énoncés clairement révisés, les méthodes formelles deviennent plus compatibles avec le développement logiciel itératif. Si chaque changement déclenche une recherche incontrôlée ou des réécritures généralisées, l’adoption restera concentrée dans des niches à haute assurance.

Les travailleurs du savoir devraient observer le même schéma dans leurs propres systèmes d’IA. L’avantage durable ne viendra pas de la production d’un plus grand nombre de brouillons. Il viendra de la construction de garde-fous d’acceptation qui restent fiables lorsque les documents, politiques, données et équipes changent.

L’automatisation des preuves Lean offre un exemple particulièrement clair parce que la génération et la vérification y occupent des rôles distincts. Le LLM peut être créatif, incohérent et parfois erroné. Le noyau exige toujours un artefact formel valide.

Cette conception ne résout pas tous les problèmes liés au travail généré par IA. Elle établit toutefois un meilleur principe par défaut : laisser les modèles proposer, laisser des systèmes explicites vérifier et laisser les personnes posséder la spécification.

La question pratique suivante n’est pas de savoir si chaque lieu de travail devrait adopter Lean. Elle consiste à déterminer quelles affirmations récurrentes méritent une vérification plus solide qu’un paragraphe assuré ou qu’un test sommaire. Identifiez une hypothèse coûteuse, reliez-la aux éléments qui l’étayent, puis demandez-vous quelle barrière déterministe pourrait la contrôler avant toute action. Cet exercice révèle où l’IA peut accélérer le travail en toute sécurité et où la relecture humaine assume encore l’intégralité de la charge. L’automatisation des preuves Lean a rendu l’objectif plus visible, mais les organisations doivent toujours choisir les affirmations qui méritent d’être démontrées.