Timbuk est un cadre de vérification régulier basé sur les Automates d'Arbres et les Systèmes de Réécriture de Termes. Il fournit un ensemble de bibliothèques pour créer et manipuler des Automates d'Arbres et des TRS, effectuer une analyse de faisabilité à l'aide de l'Algorithme de Complétion, et calculer des abstractions capables de vérifier des propriétés de sécurité sur des programmes fonctionnels de haut niveau.