Agent-oriented conceptual modelling notations such as i* have received considerable recent attention as a useful approach to early-phase requirements engineering. Agent-oriented conceptual modelling notations are highly effective in representing requirements from an intentional stance and answering questions such as what goals exist, how key actors depend on each other and what alternatives must be considered. Formal methods such as those based on the Z notation offer a complementary set of representational facilities. This paper explores how these two otherwise disparate approaches might be used in a synergistic fashion.