Context-aware systems have been in the research epicenter for more than a decade. By sensing, reasoning and acting on various kinds of relevant situational information, context-aware systems can make well-informed decisions and manifest autonomous behavior through pre-defined and user customizable rules that define what to do in particular circumstances. However, there is still a significant gap between deploying such context-aware systems in lab environments under ideal circumstances and deploying them in the real world with non-specialist end-users. These end-users may experience a lack of understanding or frustration when a system does not behave as expected, especially in the presence of unforeseen human interventions, exceptional circumstances and unexpected events. This paper investigates challenges and opportunities of using model checking as an approach for improving the reliability and consistency of smart environment applications whose behavior is driven by context-aware adaptation rules, and reports on initial results with the SPIN model checker.