Comment prouver mathématiquement qu'un programme est 100 % sans bug sans jamais l'exécuter ? La science de la vérification formelle