In this book, we have provided guidance on using Tamarin and have given illustrations of its use. In this chapter, we turn to the question of how Tamarin can be used on substantial, real-world protocols and, in particular, our experience with such large-scale verification efforts and the associated benefits. The examples we give, TLS, 5G Authenticated Key Agreement, and EMV, are substantial in terms of both their specifications’ size and complexity, and their practical relevance. TLS underlies most secure communication in the Internet between clients (computer, browsers, etc.) and servers, 5G is the predominant protocol used for cellular communication, and EMV governs most electronic payments made using credit and debit cards. Given the size of these specifications, we will only highlight what was accomplished and the lessons learned, and we provide pointers to the literature for further details.