Building secure communication systems requires both secure cryptographic primitives and also secure cryptographic protocols that build messaging schemes on top of those primitives. Well-designed protocols are the backbone of almost all modern digital communication, enabling key exchange, entity authentication, secure channels, and anonymous messaging. On the other hand, improperly designed protocols can render the best cryptography useless, for example, if the protocol inadvertently leaks a secret key. Because cryptographic protocols are simultaneously critical to our infrastructure and extremely difficult to get right, the formal verification community has spent over two decades developing tools and techniques to validate the correctness of protocol designs. The field has progressed to the point where very few scientific barriers prevent us from formally verifying all of the new protocols we develop. Despite this, we still have a long way to go on the adoption curve. Let’s take a look at what protocols verification is happening today and who is doing it. Perhaps more importantly, let's also look at who isn’t verifying their cryptographic protocols and examine potential solutions for closing the gap. At a most basic level, formal verification techniques aim to give a precise mathematical meaning (or semantics) to real-world processes and objects. This semantics captures how these entities behave and provides an environment for verifying, with mathematical precision, what is and is not true of a system. So long as the encoding is accurate, properties proven over the semantics should hold over the real system. In the case of cryptographic protocols, we seek to prove properties like the absence of man-in-the-middle attacks, data leaks, and privacy violations. When we formally verify a protocol, we establish a resilience to these kinds of flaws against an adversary with a particular set of capabilities. It’s impossible to verify protocols correct with respect t