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.