Cryptol is an open source pure functional language for expressing and reasoning about bit-precise computations, particularly cryptographic algorithms. Like Haskell, it is built upon a polymorphic, static type system, and offers similar mathematical function and sequence comprehension notation. The type system features size polymorphism and arithmetic type predicates designed to express the constraints that naturally arise in cryptographic specifications. The advanced type system and restricted domain of Cryptol enables a theorem-driven development style: correctness properties can be expressed directly in the language in tandem with the development of a specification. As the specification evolves, these properties can be continually fuzz-tested with random QuickCheck-style testing, and even sent to external SAT and SMT solvers for a mathematical proof of correctness. In this workshop, I’ll give a quick introduction the Cryptol language geared toward folks with a working knowledge of typed functional programming. Together we will implement a classical cryptosystem to learn the basic syntax and semantics of the language. As we program, we will express and check correctness properties about our implementations using QuickCheck and SMT. Finally, I will demonstrate a Cryptol specification of the ZUC stream cipher used in 4G LTE communications, and show how the theorem-driven development approach reveals a bug that required a revision of the cipher.