L'analyse flots de données est une technique d'analyse statique qui détermine des informations sur la propagation des données lors de l'exécution d'un programme informatique, sans exécuter le programme. Ces informations peuvent être notamment utilisées pour optimiser le programme lors de sa compilation. Réaliser une analyse flots de données consiste en général à résoudre un système d'équations. En dehors des méthodes traditionnelles utilisées pour résoudre de tels systèmes, d'autres techniques ont été développées. L'une d'entre elles, qui a été proposée par Bourdoncle en 1993, consiste à pré-calculer une stratégie de résolution de manière à résoudre ensuite le système plus efficacement. Cette thèse vise à développer des solveurs formellement vérifiés, qui se basent sur cette technique de résolution. Premièrement, nous proposons une formalisation rigoureuse de la notion de tri topologique faible (WTO) qui permet de représenter la stratégie pré-calculée. Ensuite, nous implémentons et vérifions formellement avec l'assistant de preuve Rocq deux variantes de résolution proposées par Bourdoncle, appelées stratégies itérative et récursive, ainsi que l'algorithme le plus utilisé pour calculer un WTO. Notre développement est entièrement intégré au compilateur formellement vérifié CompCert. Enfin, nous évaluons expérimentalement nos implémentations, en les comparant aux solveurs de CompCert et à une implémentation non vérifiée du calcul du WTO.