&Truth lève 70 millions de dollars en financement d’amorçage pour créer une machine universelle de vérification du code

&Truth, une société d’intérêt public qui développe une technologie destinée à prouver mathématiquement qu’un logiciel est sûr, a révélé publiquement ses activités le 29 octobre 2026, annonçant un financement d’amorçage de 70 millions de dollars et son projet de créer ce qu’elle appelle une machine universelle de vérification du code.

Dans son annonce de lancement, l’entreprise a indiqué avoir été fondée au début de 2026 et avoir reçu 70 millions de dollars de financement d’amorçage d’un groupe qu’elle a décrit comme réunissant des figures de premier plan de la sécurité de l’IA et du capital-risque. Elle a précisé que sa machine de vérification est conçue pour lire du code dans n’importe quel langage de programmation et prouver mathématiquement qu’il est sûr, sécurisé et correct, au moyen de preuves que chacun peut vérifier de façon indépendante.

L’automatisation des preuves fondée sur Lean

La vérification formelle existe depuis des décennies, mais elle était jusqu’à présent coûteuse et difficile d’accès, selon l’annonce, car les spécialistes devaient formuler les preuves manuellement, ce qui limitait cette pratique à quelques systèmes critiques. L’entreprise a déclaré que l’IA accélère désormais d’au moins 100 fois le travail de preuve formelle et que sa technologie d’automatisation des preuves accélère encore le processus de 100 fois, ramenant la génération de preuves de plusieurs années ou mois à quelques heures ou minutes.

L’entreprise a également présenté ce qu’elle appelle une technologie de « fabrique de spécifications », qui, selon elle, permet aux entreprises et aux développeurs de traduire à grande échelle les intentions humaines et les exigences métier en spécifications formelles précises. Il en résulte des garanties vérifiables de façon indépendante, plutôt que fondées sur des tests ou sur les déclarations des fournisseurs.

&Truth s’appuie sur Lean, un système de preuve libre, et sur Mathlib, une bibliothèque de plus de deux millions de lignes de définitions et de théorèmes mathématiques, ainsi que sur des technologies libres telles que CSLib. Selon l’entreprise, l’objectif est de créer un vocabulaire formel universel pour les logiciels : des modèles mathématiques des langages de programmation et des systèmes, des techniques de preuve et des spécifications précises permettant la vérification automatisée dans différents langages. &Truth a indiqué travailler avec le Lean Focused Research Organization et prévoir de publier ses bibliothèques fondamentales en libre accès.

Clark Barrett, cofondateur et codirecteur général, a déclaré que Lean et Mathlib fournissaient à l’IA un langage précis pour raisonner en mathématiques, mais que les logiciels ne disposaient pas d’un fondement équivalent. Ilya Sergey, cofondateur et directeur scientifique, a affirmé que la confiance dans les logiciels devait reposer sur des preuves vérifiables de façon indépendante, et non sur la parole d’une entreprise.

Fondateurs et sièges sociaux sur deux continents

Barrett est titulaire de la chaire Corbel d’informatique à Stanford University, codirecteur fondateur du Stanford Center for AI Safety, directeur du Stanford Center for Automated Reasoning, cocréateur de CSLib et responsable du projet de moteur de raisonnement automatisé cvc5. Sergey a fondé le VERSE Lab à la National University of Singapore et a cocréé les outils libres de vérification Veil et Velvet. Chris Hsu, cofondateur, codirecteur général et président exécutif, siège au conseil consultatif stratégique du Lean FRO et préside l’Infinitude Foundation. Il a auparavant été directeur général de Kilometre Capital et directeur général de Citadel Investment Group.

L’annonce a également cité Gregory Malecha, qui a précédemment dirigé les méthodes formelles chez BlueRock Security et joué un rôle essentiel dans la conception du cadre de vérification BRiCk ; Sebastian Ullrich, coarchitecte de Lean 4 et cofondateur du Lean Focused Research Organization ; Linus Lee, ancien associé directeur chez Kilometre Capital ; et Drew Harman, ancien directeur commercial de Fastino Labs et associé opérationnel chez Insight Partners et Shasta Ventures. &Truth a indiqué s’appuyer sur des décennies de recherche en vérification formelle et en raisonnement automatisé menées à Stanford University et à la National University of Singapore.

Le siège social américain d’&Truth se trouve à Palo Alto et son siège international à Singapour, où, selon l’entreprise, ses activités de recherche, d’ingénierie, de développement de produits et de commercialisation vont prendre une ampleur considérable. Dans l’annonce, Low Jin Yong, vice-président senior et codirecteur de Digital Industry Singapore, a déclaré que ce siège renforcerait les capacités de Singapour en matière de confiance et de sécurité et contribuerait à faire du pays une base pour les entreprises qui développent une IA digne de confiance.

Le site web de l’entreprise propose également une table ronde avec Leonardo de Moura, inventeur de Lean, vice-président et scientifique émérite chez AWS, ainsi que Simone Severini, membre du conseil consultatif stratégique du Lean FRO et ingénieur émérite chez Google.

Des essais complémentaires détaillent les raisons d’être de l’entreprise

Dans un essai complémentaire daté du 29 octobre 2026, Hsu a détaillé les tendances qui, selon l’entreprise, rendent la vérification urgente. Il a notamment cité les propos de Sundar Pichai, PDG de Google, selon lesquels 75 % du nouveau code chez Google est désormais généré par l’IA et approuvé par des ingénieurs, ainsi que les tests de Veracode de 2026, qui ont révélé que les modèles d’IA échouaient dans près de la moitié des tâches de programmation où la sécurité était en jeu. L’essai évoque également une campagne menée en septembre 2026, au cours de laquelle un attaquant a déployé des centaines d’agents d’IA pour s’introduire dans 395 organisations réparties dans 48 pays en exploitant des failles d’un logiciel de gestion d’impression largement utilisé, ainsi qu’un nombre record de 14 959 vulnérabilités logicielles publiées en septembre 2026, soit, selon l’essai, 3,5 fois le nombre publié un an plus tôt.

L’essai retrace des jalons antérieurs de la vérification formelle : la preuve initiale du micro-noyau seL4 a nécessité environ 20 années-personnes de travail spécialisé pour quelque 8 700 lignes de code ; en 2015, dans le cadre du programme HACMS de la DARPA, seL4 a été intégré à l’hélicoptère Unmanned Little Bird de Boeing, dont les commandes de vol ont résisté aux tentatives de compromission d’une équipe rouge professionnelle disposant de plusieurs semaines d’accès ; et, en septembre 2026, un modèle d’IA développé par Anthropic a formalisé dans Lean, en 11 jours, la preuve complète du dernier théorème de Fermat. L’essai relève également qu’au début de l’année 2026, Kim Morrison, ingénieur logiciel de recherche principal au Lean FRO, a utilisé Claude d’Anthropic avec un minimum de directives humaines pour créer une version de la bibliothèque de compression zlib en Lean et prouver qu’elle restitue toujours exactement les données qu’elle a compressées.

L’essai cite le créateur de Lean, Leonardo de Moura : « Les tests inspirent confiance. La preuve apporte une garantie. »

Dans un deuxième essai publié le 29 octobre 2026, Sergey explique les mécanismes de la vérification des programmes, en commençant par l’article d’Alan Turing publié en 1949, « Checking a Large Routine », qui proposait que les programmeurs accompagnent leur code d’affirmations précises qu’un vérificateur pourrait contrôler individuellement. L’essai présente les spécifications, les invariants de boucle et les preuves vérifiées dans Lean, et précise que &Truth vise à permettre aux développeurs d’obtenir des éléments probants vérifiables de manière indépendante, par exemple une preuve formelle dans Lean, à un coût qui fasse de la vérification une pratique courante du développement.

&Truth décrit sa vision à long terme comme le passage du « codage à l’instinct » au « codage vérifié », dans lequel le code généré par l’IA est vérifié mathématiquement avant son déploiement, les agents d’IA opèrent dans des environnements dont le confinement peut être démontré, les logiciels anciens sont modernisés en toute sécurité et les infrastructures critiques sont protégées par des garanties mathématiques vérifiables de manière indépendante.