Cette thèse propose des outils pour la vérification formelle de la correction de circuits matériels. Pour la vérification de la correction d'un circuit combinatoire par rapport a sa spécification, une nouvelle méthode pour spécifier des fonctions booléennes est présentée, les systèmes de réécriture booléens (BTRS), puis une transformation d'un BTRS en deux expressions booléennes est décrite qui permet de vérifier la correction, la complétude et la cohérence d'une spécification par rapport a une implémentation. Pour la vérification de circuits séquentiels, deux nouveaux algorithmes qui décident l'équivalence et l'inclusion de deux machines de mealy sont introduits. Ces problèmes de décision peuvent aussi être vus comme cas spécifiques de la vérification d'un invariant d'une machine, a savoir la machine produit. Un survol uniforme et généralise sur les méthodes d'itération de point fixe décrit l'analyse de l'atteignabilité d'une machine et le test de la non-atteignabilité d'un ensemble d'états. Ces algorithmes de test d'équivalence et d'inclusion sont implémentes dans le logiciel fancy. Finalement, les applications en preuve de circuits des démonstrateurs de théorèmes généraux sont explorées. Une méthode de description et de preuve des circuits paramètres combinatoires ou séquentiels par des systèmes de réécriture est présentée. Différentes sortes de preuves qui ont besoin de telles descriptions sont montrées: par réécriture (prouveurs lp ou reve), par induction (lp), par consistance (reve), par des ensembles tests (spike)