This work presents our approach to formally model the Swiftaid system design, a digital platform that enables donors to automatically add Gift Aid to donations made via card payments. Following principles of Behaviour-Driven Development, we use Gherkin to capture requirements specified in legislation, specifically the UK Charity (Gift Aid Declarations) Regulations 2016. The Gherkin scenarios provide a basis for subsequent formal modelling and analysis using Event-B, Rodin and ProB. Interactive model simulations assist communication between domain experts, software architects and other stakeholders during requirements capture and system design, enabling the emergent system behaviour to be validated. Our approach was employed within the development of the real Swiftaid product, launched by Streeva in February 2019. Our analysis helped conclude that there was not a strong enough business case for one of the features, which was shown to provide nominal user convenience at the expense of increased complexity. This work provides a case study in allying formal and agile software development to enable rapid development of robust software.