Tests logiciels ou vérification formelle – l’importance décisive de la preuve mathématique

Dans cet extrait d'Elektor Engineering Insights n°54, j’ai posé à Quentin Ochem de AdaCore la question évidente mais agaçante : pourquoi ne pouvons-nous pas simplement tester les logiciels pour tout et nous en contenter ?

Comme le souligne Quentin, même une petite fonction manipulant deux entiers nécessiterait un nombre astronomique de cas de test pour couvrir toutes les possibilités. Vous pourriez tester jusqu’à la fin de l’univers sans jamais tout épuiser. Les métriques de couverture, le fuzzing, l’analyse des limites — tout cela aide, bien sûr, mais aucune de ces approches ne peut prouver la correction d’un programme.

La vérification formelle, en revanche, le peut réellement. Avec SPARK, vous pouvez démontrer mathématiquement que votre code se comporte exactement comme l’exige la spécification, et ce dans 100 % des cas. Ce niveau de certitude peut sembler excessif en matière de sûreté, où une fiabilité de type “neuf neufs” est parfois jugée suffisante selon les coûts. Mais pour la sécurité, il suffit qu’un attaquant trouve une seule faille dans dix millions de lignes de code : la preuve l’emporte alors toujours sur la probabilité.

Quentin a aussi évoqué l’arrivée de l’IA dans ce domaine — non pas pour remplacer les analyseurs statiques, mais pour les renforcer grâce à de nouvelles méthodes de détection de bugs, voire de suggestion de corrections. Je lui ai répondu que je n’y croirai que le jour où mon IDE cessera de me harceler au sujet des points-virgules manquants.

Tests logiciels vs. vérification formelle

La vérification formelle peut sembler relever du perfectionnisme académique, mais l’argument de Quentin est limpide : lorsque les attaquants n’ont besoin de trouver qu’un seul bug, les chances ne jouent pas en votre faveur si vous ne comptez que sur les tests. Des outils comme SPARK déplacent l’argument de la probabilité vers la certitude, et cela soulève des questions pour tous ceux qui écrivent du code — des développeurs embarqués aux équipes logicielles sous pression constante pour livrer. J’aimerais savoir ce que vous en pensez : la preuve est-elle l’avenir, ou la plupart d’entre nous vont-ils encore se contenter de « suffisamment testé » ? Partagez vos avis dans les commentaires.