This paper presents \emph{verification-guided development} (VGD), a software development process that we used to develop Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves two activities: (1) writing a readable, executable model of the system and proving mechanically-verified properties about it; and (2) writing production code for the system, using extensive \emph{differential random testing} (DRT) to check that the production code’s behavior matches that of the model, and \emph{property-based testing} (PBT) to check properties of unmodeled components of the production code. Using VGD for Cedar has been beneficial: we are able to build fast, idiomatic production code and find and fix bugs during the development phase: when carrying out proofs we found and fixed four soundness bugs in Cedar’s policy validator, and when carrying out DRT and PBT we found and fixed 21 bugs in the Cedar parser, evaluator, authorizer, and validator.