Hazel est un projet de formalisation Coq visant à vérifier des bibliothèques d'analyse numérique, telles que l'analyse définie par la règle et la différentiation automatique. Il définit un langage de programmation formel avec des effets et développe une logique de programmes pour raisonner sur les programmes qui peuvent effectuer des effets.

GeoCoqInE-Euclid est un projet de démonstration de théorèmes géométriques automatisée, utilisant le langage de programmation fonctionnelle Coq et la bibliothèque Euclid. Il permet le développement et la vérification de preuves formelles, ainsi que le travail collaboratif sur des théories mathématiques.