The role of formal methods to add precision in the design and analysis of systems has been demonstrated in a wide range of contexts. They are particularly valuable in the case of safety-critical systems but also in the many systems where failure to use or to understand a system can cause substantial costs. This chapter provides an overview of work on the application of Formal Methods to Human-Computer Interaction. The focus is on the type of modeling and analysis that can be used to reason formally about the interaction between a system and its users as well as the role that this analysis can have in ensuring the quality of an interactive system. The review is organized around five layers of modeling that capture the range of perspectives in which analysis can be performed. An example is used to give some notion of what is involved in performing formal verification of interactive systems, from defining the models to identifying, formally expressing and analyzing use-related requirements.