Authentication to digital systems using passwords—secret knowledge used by a claimant to authenticate their identity to a second party (the verifier)—remains dominant today despite decades of research into alternative authentication factors and repeated predictions that passwords will soon die out. While they exhibit a number of very desirable security properties, human-chosen passwords remain vulnerable to guessing attacks, and a number of measures have been designed to motivate users to create less predictable passwords as well as make guessing attacks more difficult to carry out for attackers. These measures, known as password policies, restrict different aspects of password creation, usage and management with the goal of enhancing their security. In this work, we apply statistical techniques and formal methods to the design, development and deployment of password policies, with a particular focus on policies governing password composition and lockout measures designed to arrest the evolution of password guessing attacks against live systems. In doing this, we present an end-to-end workflow beginning with sourcing and cleansing human-chosen password data upon which to experiment, employing this data in the design of password policies, and finally developing formally verified software capable of enforcing these policies on real-world digital systems.