Outil dédié à l'analyse et à l'optimisation de modèles de compteurs abstraits utilisés en vérification formelle. Il permet de déterminer des tailles de ensembles concrets à partir de modèles pseudo-booléens, facilitant ainsi la validation de propriétés logiques complexes. Développé dans le cadre du projet BLaSST, il s'intègre dans des workflows de preuve automatisée pour les systèmes critiques.