Les équations différentielles sont utilisées dans de nombreux domaines afin de modéliser des phénomènes physiques et biologiques. Malheureusement, leur résolution exacte n'est pas toujours possible, ce qui conduit à l'utilisation de méthodes numériques qui en donnent des solutions approchées. Ces méthodes, souvent complexes, mènent à deux sources d'erreurs: les erreurs de méthode dues aux approximations qu'elles induisent et les erreurs d'arrondi résultant de leur implémentation avec des nombres à virgule flottante. Nous exhibons des bornes à grain fin sur les erreurs d'arrondi de méthodes itératives comme les schémas de Runge-Kutta appliquées à des systèmes linéaires multidimensionnels et gérons les comportements exceptionnels (dépassements de capacité inférieurs et supérieurs). Par ailleurs, afin de garantir un haut niveau de confiance dans ces résultats, nous en formalisons une partie dans l'assistant de preuves Coq.