Projet open source permettant de transformer du code écrit en WhyML, un langage de spécification et de preuve, en code Java exécutable. Il facilite la vérification formelle de propriétés logiques sur des algorithmes tout en produisant un code source compatible avec l'écosystème Java. Utilisé principalement dans le domaine de la recherche académique et de la validation de programmes.