A partir du 1er juillet 2017, l’action InriaSoft de la fondation Inria proposera aux utilisateurs de COQ d’adhérer à un consortium qui se bâtit pour soutenir le logiciel.

Le logiciel COQ est un assistant de preuves pour la vérification de théorèmes et de programmes. Il est le fruit de très nombreuses années de R&D menées au sein de l’institut Inria en collaboration avec ses partenaires.