Ce projet propose un cadre automatisé pour la vérification formelle de circuits matériels complexes. Il permet de vérifier des propriétés temporelles et de prouver des lemmes sur des architectures électroniques, notamment via des techniques de model-checking symbolique et de preuve automatique. L'objectif est d'améliorer la fiabilité et la robustesse des systèmes embarqués en détectant des erreurs de conception avant leur déploiement.

Kôika-SUSHI est un langage de conception matérielle basé sur des règles, intégré dans Rocq. Il permet de développer et de vérifier formellement des circuits électroniques, notamment des processeurs. Ce projet facilite la création de matériel fiable et optimisé grâce à des preuves mathématiques intégrées, en s'appuyant sur des approches de réécriture progressive et des outils SMT pour renforcer la robustesse des designs.

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.