Coq est un assistant de preuve, c’est à dire un langage formel pour décrire des définitions mathématiques et des outils pour vérifier formellement des algorithmes ou des théorèmes, si nécessaire de manière interactive. Ce logiciel est souvent utilisé pour faire de la preuve de programmes (par exemple dans le cadre du compilateur C certifié comp-cert), mais aussi pour formaliser les mathématiques et pour l’enseignement. Le projet a démarré en 1984 et concerne les sciences du numérique et des mathématiques.