Real World Verification - Experiences from the Verisoft Email Client Gerd Beuster, Niklas Henrich, and Markus Wagner This paper reports our experiences developing a completely verified email client. The formal specification of the email client includes all informal requirements and security goals. Compliance to the formal specification has been proven for the complete source code. The email client is part of project Verisoft, where pervasively verified systems are developed.