El papel del usuario en una formalización típica con ACL2 consiste en: a) definir las funciones que implementan el sistema que se quiere verificar, b) escribir la especificación del mismo, expresando las propiedades formales que se desean verificar y c) guiar al demostrador hacia una demostración automática de dicha especificación.