Abstract: In this paper we demonstrate usability analysis of Object-Z user-interface designs. Usability can be defined in terms of five salient properties of an interactive system: task efficiency, reuse, user-computer communication, robustness and flexibility. Formal user-interface designs have been advocated as a basis for determining the usability of an interactive system prior to the expense of system development. However to date, a comprehensive demonstration of the utility of formal designs for this purpose has not been forthcoming. We investigate the limitations of model-based methods, such as Object-Z, as a basis for analysis of user-interface designs.