HOL-OCL est un système de preuve (basee sur Isabelle/HOL) pour des spécifications object-orientées en UML/OCL. On peut analyser des systèmes des contraintes en OCL, établir des raffinements formelles entre des packages et vérifier des programmes simples sur base des contracts en OCL.