We present a case study on the development of a formally verified PHP web social network application. With the expansion of social media and our presence in the cyber world, the privacy and security of our content online have become a great concern. Our goal was to investigate whether we could formally verify privacy policies of a social network using the Event B method. We chose to build a formally verified social network application for the following reasons: formally verifying the model with privacy policies shows consistency between the visibility of the user’s content and the privacy setting of that content, and the privacy policies are readily formalized. The project involved building an Event-B model for the application in the Rodin environment, verifying that the user’s data is visible to the correct set of people in the network using Rodin’s automated theorem provers, and translating the model from Event¬ B to PHP code using the EventB2SQL tool. We also extended the EventB2SQL tool to generate the user interface components, reducing the amount of code that needed to be completed by hand. The end product of this project is an application that resembles a real-world social network. By developing a formally verified software system, we confirmed Event B’s ability to build models in the area of social network privacy policies.