Malware is a serious problem on mobile devices. Our vision is a verified app store in which each application has been formally proven to be free of (certain) defects and exploits. We have built such a system and successfully applied it to dozens of challenge applications created by hostile Red Teams. This talk describes our type system for information flow, along with support for implicit invocation (intents and reflection), varieties of polymorphism, and other challenges that arose.