System-Theoretic Process Analysis (STPA) from Leveson is a technique for hazard analysis developed to identify more thoroughly the causal factors in complex safety-critical systems, including software design errors. Event-B is a proof-based modelling language and method that enables the development of specifications using a formal notion of refinement. We propose an approach to hazard analysis where system requirements are captured as monitored, controlled, mode and commanded phenomena and STPA is applied to the controlled phenomena to identify systematically the safety constraints. These are then represented formally in an Event-B specification which is amenable to formal refinement and proof.