Recent years have seen the emergence of a number of research groups that aim to advance quantum computing and to develop a skilled quantum software workforce. A particular challenge that must be overcome for safe quantum computing at scale is the creation of robust, expressive, efficient, and tractable formal verification tools. Since there is currently no event dedicated to this pursuit, the first goal of this Dagstuhl Seminar is to bring together a dedicated community of researchers in a single venue. This will give participants an opportunity to identify and discuss the most pressing challenges and promising directions for quantum programming and verification.