Cadre de travail Coq dédié à la conception et à la vérification formelle de contrôleurs de mémoire DRAM. Permet aux chercheurs et ingénieurs de modéliser des architectures mémoire complexes et de valider leur comportement à l'aide de preuves formelles. Utilisé dans le cadre de travaux académiques ou industriels pour garantir la fiabilité des systèmes mémoire.