Le prouveur de théorèmes haRVey implante une procédure de décision pour les formules équationnelles non quantifiées dans des théories des tableaux. Ce travail étudie son applicabilité à la vérification, par construction d'invariants, de propriétés de sûreté exprimées sur des systèmes paramétrés. La correction du programme paramétré doit être assurée pour toutes les valeurs des paramètres, interdisant le model-checking. Elle peut s'entreprendre par un calcul de point fixe dont les conditions d'évolution sont déchargées dans un prouveur supportant les formules quantifiées. Graf et Saïdi ont ouvert cette voie en exploitant le prouveur PVS. D'autres ont suivi en exprimant leur système à l'aide de contraintes arithmétiques linéaires obtenues par une abstraction de comptage. Nous proposons un cadre plus basique mais unificateur où les paramètres sont des ensembles finis. Nous montrons que ce cadre convient pour des exemples industriels et des systèmes uniformes distribués. Les spécifications sont écrites dans le langage des machines abstraites B et nous exploitons les calculs de plus faible précondition déjà définis pour cette méthode. Nous introduisons ensuite un calcul de point fixe, obtenu par raffinement d'un calcul de point fixe trivial. Nous proposons ensuite diverses traductions en logique équationnelle des conditions d'évolution, dans l'objectif de faire converger le plus rapidement le prouveur haRVey qui les décharge. Nos expérimentations sur un exemple industriel montrent que la démarche supplante celle du prouveur de l'Atelier B. Théoriquement, nous montrons la décidabilité de certaines obligations de preuve dans le cadre de systèmes uniformes distribués.