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.