Ce document présente l'étude de la relation entre la preuve de programmes parallèles et le raffinement de spécifications formelles en programmes parallèles (ou communicants). Il vise à intégrer les systèmes axiomatiques de preuve dans la démarche de construction pas-à-pas de programmes parallèles à partir de spécifications formelles, telles que les propriétés d'invariance et de fatalité. Nous avons dégagé des transformations relatives à des classes de programmes (parallèles) à partir d'études de cas. La relation de raffinement est fondée sur la préservation des propriétés déjà acquises ou démontrées. Elle admet une sémantique exprimée à l'aide des transformateurs de prédicats spécifiques à la classe considérée mais elle admet une autre sémantique fondée sur le système formel lui-même et sur la notion de preuve. Les transformations sont correctes par rapport à ces deux sémantiques équivalentes. La thèse de ce document peut se résumer comme suit: raffiner un programme en un autre programme suivant une sémantique de transformation de prédicats revient à raffiner la spécification du programme selon les règles du système formel construit à l'aide des transformateurs de prédicats. La structuration des informations à manipuler a conduit à proposer un langage pour les termes de développement comprenant, pour chaque terme, la spécification, la documentation formelle, le programme et l'environnement. Le lieu entre les différents termes est défini par la relation de raffinement (en accord avec les transformateurs de prédicats ou en accord avec les règles)