Coq est un système de gestion de preuves formelles. Il offre un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves machine-checkées.