Sukerujo est un système de déduction pour le lambda-calcul et les démonstrations formelles. Il permet de vérifier des preuves, d'inférer des types pour des expressions lambda, et d'analyser les dépendances entre modules.