Un outil d'IA de Stanford a vérifié une partie du code de Signal en une demi-journée et pour 500 $, contre 5 mois

La vérification formelle, c'est-à-dire la preuve mathématique qu'un programme fait exactement ce qu'on attend de lui, est restée pendant des décennies l'apanage de passionnés et des systèmes les plus critiques. Aujourd'hui, l'IA générative tente d'en faire un outil ordinaire. La chercheuse de Stanford Chuyue Sun et ses collègues ont montré dans un article récent que leur outil d'IA avait mené à bien un projet d'ingénierie en moins d'une demi-journée et pour moins de 500 $. Trois experts hautement qualifiés avaient consacré cinq mois au même travail. Le projet concernait une partie du code qui chiffre les conversations de la messagerie Signal.

Pourquoi les maths coûtent soudain moins cher

La vérification classique est difficile pour deux raisons. Les ingénieurs doivent consigner avec précision ce qu'ils attendent du programme, puis traduire le code en formules vérifiables. Les entreprises font déjà tourner des tests complexes, mais investissent rarement dans la vérification formelle, bien qu'elle détecte des défaillances plus tordues.

Les nouvelles startups misent sur l'automatisation de la première étape. L'IA doit rédiger les spécifications : pour le tri d'un tableau, par exemple, elles exigent que l'ensemble des éléments soit identique avant et après, seul l'ordre changeant. La traduction ultérieure du code vers le format des assistants de preuve Lean, Rocq et Isabelle peut se passer d'IA.

Sun a rejoint &Truth en août ; la société a été lancée publiquement jeudi. La startup a levé 70 M$ et veut, à terme, vérifier du code dans n'importe quel langage. Le directeur scientifique de &Truth, Ilya Sergey, compare cela au bâtiment : les ponts et les immeubles ne s'effondrent pas parce qu'on les calcule en amont ; les technologies pour ce type de raisonnement sur le code existaient, mais passaient mal à l'échelle.

Qui d'autre s'intéresse à ce marché

Son concurrent Harmonic, cofondé par le patron de Robinhood Vlad Tenev, a levé 295 M$. Cette semaine, l'entreprise a annoncé que son agent d'IA pour les mathématiques, Aristotle, sait vérifier des logiciels en C et des descriptions matérielles en Verilog. La technologie est évaluée par des clients potentiels, dont le fabricant de puces Tensordyne et Nvidia, dont le fonds de capital-risque figure parmi les investisseurs de Harmonic.

Une semaine plus tôt, Anthropic et la startup Theorem avaient indiqué avoir utilisé l'IA pour trouver, dans des logiciels open source, des erreurs qui avaient échappé à des trillions de tests. Elles ont aussi publié une extension de Claude pour aider les développeurs à vérifier leur code. Le coût du premier projet n'a pas été divulgué. Madan Musuvathi, parti de Microsoft Research après plus de 20 ans, a fondé Truidic : selon lui, l'IA est très puissante entre les mains des attaquants, et la vérification peut rendre les systèmes d'IA sûrs.

La Beneficial AI Foundation, grâce à une subvention d'Anthropic, a vérifié cette année le même code cryptographique que Sun. Michael Rosenberg, mainteneur de la bibliothèque curve25519-dalek, espère un financement durable, mais ne sait pas d'où il viendra, et juge malvenu de dépendre de la bonne volonté des entreprises d'IA.

Scepticisme et limites

La vérification est déjà présente dans les avions de Boeing, les serveurs d'Amazon et plus de 2,5 milliards d'appareils actifs d'Apple, mais il s'agit en général de code lié à la sécurité. Byron Cook, d'AWS, affirme que la méthode a levé une partie des inquiétudes des clients du cloud et accéléré les équipes internes. En revanche, plusieurs entreprises de taille moyenne ont confié à WIRED n'avoir vérifié qu'une seule fonction clé, au maximum.

Les raisons : manque de spécialistes, coût supérieur aux risques éventuels et crainte que des semaines d'attente ne ralentissent la sortie du produit. Deux responsables cybersécurité de grandes entreprises, qui n'ont jamais vérifié de code formellement, ne sont pas certains que l'automatisation changera le calcul, mais sont prêts à payer les grands laboratoires d'IA pour du code généré « vérifié ».

La technologie en est encore au stade de prototype. On ignore combien les clients sont prêts à payer et comment ils veulent l'adopter : directement ou via des intermédiaires comme Anthropic. La méthode repose sur des hypothèses quant à la façon dont ordinateurs et humains interagissent avec les logiciels ; une partie des experts doute donc qu'elle détecte les erreurs d'utilisateurs et les pannes matérielles.

Will Wilson, patron de la startup Antithesis, qui traque les bugs grâce à l'IA, qualifie la vérification formelle de « piège » pour les mathématiciens comme lui. L'entreprise a dépensé des millions de dollars pour vérifier une partie de sa protection, a décrit le processus comme douloureux et a malgré tout trouvé des erreurs supplémentaires avec son propre outil. Antithesis a aussi détecté des bugs dans des logiciels de clients déjà vérifiés. Selon lui, la vérification formelle apporte une certaine confiance, mais seuls des tests exhaustifs peuvent la confirmer. Vitalik Buterin a lui aussi écrit sur son blog qu'elle n'est pas une panacée.

Une autre réserve concerne les spécifications elles-mêmes. Les fondateurs de Proofcraft, June Andronick et Gerwin Klein, disent que l'intérêt dépasse leurs capacités et celles de leurs concurrents, mais redoutent une « confiance injustifiée » dans les résultats obtenus avec des spécifications écrites par IA. Pour les équipes, la conclusion pratique est la suivante : l'IA rend la vérification assez bon marché pour l'essayer sur des modules critiques comme la cryptographie, mais elle ne promet pas de remplacer les tests.