Comment une vague de startups mise sur l’IA pour rendre la vérification formelle des logiciels pratique et indispensable, dont &Truth, lancée avec un tour d’amorçage de 70 millions de dollars

Paresh Dave / Wired · vendredi 30 octobre 2026 à 9 h 12

Une nouvelle startup, baptisée &Truth, rejoint la course à l’automatisation de la vérification formelle, un processus minutieux qui s’appuie sur les mathématiques pour prouver que les logiciels fonctionnent comme prévu.

Plus de couverture

Sur X

@andtruthpbc · Nous sommes dans le @nytimes : si l’IA peut démontrer des problèmes de mathématiques ouverts, peut-elle prouver qu’un logiciel ne contient aucun bug ? C’est ce sur quoi nous travaillons, avec Lean comme fondement d’une confiance vérifiée par machine. https://www.nytimes.com/...

Sur Bluesky

@druce.ai · La vérification formelle, qui prouve mathématiquement la correction du code, attire des startups comme &Truth (70 millions de dollars) et Harmonic, alors que le code écrit par l’IA se multiplie
Danny Groner / @dannygroner · « La grande promesse, c’est un avenir où les logiciels fonctionnent plus fiablement et posent moins de problèmes de sécurité. Mais la question de savoir si l’IA peut étendre la vérification formelle au-delà des systèmes les plus critiques, dans des organisations comme la NASA et Apple, et en généraliser l’usage reste ouverte. » [publication citée]

Comment une vague de startups mise sur l’IA pour rendre la vérification formelle des logiciels pratique et indispensable, dont &Truth, lancée avec un tour d’amorçage de 70 millions de dollars

Plus de couverture

Sur X

Sur Bluesky

L’essentiel du Fil