Ce projet développe des preuves formelles en Coq pour valider des modèles de mémoires tampons (store buffers) parallèles. Il explore des configurations avec verrous fins ou complets et démontre leur monotonie ou leurs contre-exemples. Les travaux servent de base théorique pour l'analyse de systèmes concurrents et la correction de protocoles de cohérence mémoire.