Coq est un assistant de preuve interactif qui permet la vérification formelle de preuves mathématiques et la spécification et vérification de systèmes informatiques. Il utilise un langage de programmation dédié, le Gallina, pour écrire des preuves et des spécifications.