HOL-Z est un système de preuve basé sur Isabelle/HOL (version 2005). Il est possible d'importer des specifications préparer en LaTeX et type-checked dans le système externe ZeTa. Le systeme genère des obligations de preuve pour l'analyse des spécifications et pour le raffinement d'un modele abstrait par un modèle plus concrete (data refinement). Le système offre des moyens habituel d'Isabelle pour prouver ces obligations.
