&Truth lance une machine de vérification universelle pour sécuriser le code logiciel

Le 29 octobre 2026, la société à but non lucratif &Truth a levé 70 millions de dollars en fonds d'amorçage et a présenté son projet de « machine de vérification universelle ». Selon l’annonce de l’entreprise, cet outil devrait pouvoir lire du code dans n’importe quel langage et produire, de façon automatisée, une preuve mathématique attestant de sa sûreté, de sa sécurité et de sa correction. Les preuves seraient vérifiables indépendamment, sans dépendre d’un test propriétaire ou d’une promesse du vendeur.

Une technologie qui s’appuie sur Lean et Mathlib

&Truth construit sa solution autour de Lean, un système de preuve open‑source, et de Mathlib, une bibliothèque contenant plus de deux millions de définitions et de théorèmes. Le « specification factory » décrit dans le communiqué permettrait aux équipes de traduire leurs exigences métier en spécifications formelles, puis de générer automatiquement les preuves correspondantes. La société affirme que l’IAIntelligence artificielleEnsemble de techniques permettant à des machines d'accomplir des tâches nécessitant habituellement certaines capacités humaines, comme la reconnaissance, la prédiction ou la prise de décision. accélère aujourd’hui le travail de preuve de 100 fois, et que son automatisation ajoute encore un facteur 100, réduisant ainsi un processus qui prenait auparavant des mois ou des années à quelques heures, voire quelques minutes.

Des fondateurs issus du monde académique et de la recherche en vérification

Parmi les co‑fondateurs, Clark Barrett occupe le poste de Corbel Professor en informatique à Stanford et dirige le Stanford Center for AI SafetyAI SafetyDomaine consacré à l'identification, à la prévention et à la réduction des risques associés aux systèmes d'intelligence artificielle.. Ilya Sergey, quant à lui, dirige le VERSE Lab de l’Université nationale de Singapour. Tous deux soulignent l’absence, à ce jour, d’un langage formel commun aux logiciels, comparable à ce que Lean et Mathlib offrent aux mathématiques. Le troisième co‑fondateur, Chris Hsu, siège au conseil stratégique du Lean FRO et a occupé des postes de direction chez Kilometre Capital et Citadel.

Pourquoi la vérification devient‑elle urgente ?

Dans un essai d’accompagnement publié le même jour, Hsu cite plusieurs signaux d’alerte : plus de 75 % du nouveau code chez Google serait généré par l’IA, selon Sundar Pichai, et les tests menés par Veracode en 2026 ont montré que les modèles d’IA échouaient sur près de la moitié des tâches de sécurité. Un incident de septembre 2026, où des agents d’IA ont compromis 395 organisations à travers 48 pays via des failles d’un logiciel de gestion d’impression, renforce le besoin d’une assurance plus solide que le simple test.

Des précédents qui montrent la voie

Le communiqué rappelle le micro‑noyau seL4, dont la preuve initiale a nécessité 20 années‑personne pour 8 700 lignes de code et a ensuite été intégré à l’hélicoptère Unmanned Little Bird de Boeing. En septembre 2026, un modèle d’Anthropic a formalisé la preuve du dernier théorème de Fermat en Lean en 11 jours, illustrant la rapidité croissante de l’automatisation des preuves. Plus récemment, un ingénieur du Lean FRO a utilisé Claude d’Anthropic pour produire une version Lean de la bibliothèque de compression zlib, prouvant que le processus de compression‑décompression restaure exactement les données d’origine.

Enjeux pour les développeurs et les entreprises

Si la promesse de &Truth se concrétise, les développeurs pourraient obtenir, à chaque commit, une preuve formelle vérifiable du respect des spécifications, sans devoir recourir à des audits manuels coûteux. Les entreprises auraient ainsi une base légale et technique solide pour garantir que leurs systèmes critiques – que ce soit dans la santé, l’aéronautique ou les infrastructures publiques – ne comportent pas de vulnérabilités cachées. Le modèle économique proposé reste flou, mais la société indique qu’elle prévoit de rendre ses bibliothèques fondamentales open‑source, ce qui pourrait favoriser une adoption progressive au sein de la communauté.

Perspectives à moyen terme

Le plan de &Truth inclut l’expansion de son bureau de Singapour, destiné à devenir un hub de recherche, d’ingénierie et de commercialisation. La présence de personnalités comme Leonardo de Moura, créateur de Lean, et Simone Severini, ingénieur chez Google, renforce la légitimité technique du projet. Cependant, la technologie reste à ce jour à l’état de démonstration ; aucune preuve publique n’a encore été présentée pour un projet logiciel de grande envergure. Les développeurs intéressés devront attendre les premiers cas d’usage avant de pouvoir juger de la robustesse et du coût réel de l’automatisation de la vérification.

La communauté open‑source observe donc attentivement les premiers livrables de &Truth, qui pourraient, si elles tiennent leurs promesses, transformerTransformerArchitecture de réseau neuronal reposant notamment sur des mécanismes d'attention pour traiter des séquences de données. la façon dont le code est certifié avant sa mise en production.