Les méthodes formelles permettent d’obtenir un très haut niveau d’assurance quant à la correction d’un développement. Leur utilisation est encouragée, et parfois exigée, lorsqu’il y a des exigences fortes en matière de sûreté de fonctionnement ou de sécurité.
Pourtant, il ne faut pas faire aveuglément confiance à un développement formel. Cet article analyse les problèmes potentiels qui peuvent se poser et identifie quelques pièges classiques à éviter lorsque des méthodes formelles déductives (telles que B, Coq, Focal, PVS, etc.) sont utilisées avec un objectif de sécurité. Il vise aussi à permettre une meilleure évaluation du réel niveau d’assurance obtenu.
