In recent years, several software verification frameworks have been applied to analyze the correctness and security of implementations of cryptographic algorithms and protocols, with some notable successes. I will describe what makes the analysis of real-world cryptography interesting and challenging for formal verification, using examples from several research and commercial projects I have participated in. We will discuss the limits of what can be proved today, what remains to be done, and what challenges I see on the horizon.