La vérification formelle mise sur l'IA pour s'imposer
Original : The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself
Pourquoi c'est important
L'automatisation de la vérification formelle pourrait réduire les failles logicielles à grande échelle.
La startup &Truth lève 70 M$ pour automatiser la vérification formelle de code grâce à l'IA. Un outil a reproduit en moins d'un jour un travail qui avait pris 5 mois à trois experts, pour moins de 500 $.
Pendant des décennies, la vérification formelle — qui consiste à prouver mathématiquement qu'un logiciel fonctionne comme prévu — est restée trop lente et coûteuse pour être adoptée à grande échelle. L'IA générative pourrait changer la donne. La chercheuse de Stanford Chuyue Sun a publié un article montrant qu'un outil IA a vérifié une partie du code de chiffrement de Signal en moins d'une demi-journée pour moins de 500 $, contre cinq mois de travail pour trois experts humains. Elle a rejoint &Truth, lancée publiquement ce jeudi, qui vise à terme à vérifier n'importe quel langage de programmation. Côté concurrence, Harmonic — cofondée par le PDG de Robinhood Vlad Tenev et dotée de 295 M$ — a annoncé que son agent IA Aristotle supporte désormais C et Verilog, avec Nvidia parmi ses investisseurs. Anthropic et la startup Theorem ont également révélé avoir détecté des bugs dans des logiciels open source que des milliers de milliards de tests avaient manqués. Malgré l'enthousiasme, la technologie reste au stade du prototype. La demande est forte, mais les modèles tarifaires et les modes d'adoption restent flous.