COQQTL est un projet visant à porter l'intermédiaire de représentation FIRRTL pour les langages de description matérielle (HDL) dans l'assistant de preuve Coq. Il permet de vérifier formellement des circuits électroniques en utilisant des méthodes de preuve mathématique, garantissant ainsi leur correction et leur fiabilité. Le projet s'adresse principalement aux chercheurs et ingénieurs en électronique et en informatique qui souhaitent valider des architectures matérielles de manière rigoureuse.