Outil en ligne de commande conçu pour prouver des obligations de preuve au format POG en utilisant la plateforme Why3. Il permet de transformer des fichiers de preuve en formats compatibles avec divers prouveurs automatiques (Zenon, SMT-LIB, TPTP, etc.) pour valider des théorèmes mathématiques ou des propriétés logiques. Idéal pour les chercheurs et développeurs en vérification formelle ou en logique mathématique.