This project is a case study on formal verification of an Android application used for pain management. When it comes to healthcare applications, the consistency of the application is crucial, as it may affect the wellbeing of the user. The application will check for trends in the user reports of pain, stress, etc. and notify the user accordingly. The model that specifies these trends is defined in Event-B using an Eclipse-based IDE called Rodin. We used the automated and interactive theorem provers built into Rodin to verify that the model always gives the user consistent information. The Event-B model is translated from Event-B to Java using the EventB2SQL tool. The Java class generated from the model forms the core of our Android application. We have recently extended the EventB2SQL tool to generate Android user interface components, further facilitating the development of our application. Since the model is based on a formally verified Event-B model, we can say with confidence that the application will not output any harmful or misleading information to the user. This paper will further elaborate on the research we are doing in Event-B, EventB2SQL, and the advantages of formal verification for a healthcare application.