One of the central questions of formal verification asks: does this program do what it’s supposed to? Built into this simple idea are more subtle underlying questions: How do we precisely specify a program’s intended behavior? How do we formally reason about what the program actually does? And how do we rigorously and efficiently verify that these two notions align?

In the interdisciplinary field of quantum computing, answering these questions requires particular nuance. Researchers from different backgrounds bring different perspectives on both specification and analysis. A quantum program’s specification can be expressed as a probability distribution over measurement results, as a complex matrix of exponential size, or as an abstract categorial diagram. A program’s semantics can be described by an idealized step relation, or more realistically, can incorporate noise models, decoherence, and the physical constraints of state-of-the-art quantum computing hardware.

This talk will explore what it means for a quantum program to “do what it’s supposed to”: how to specify correctness; how to analyze actual behavior; and how formal verification can bridge the gap between them. Luckily, we can draw on a rich toolbox of classical formal methods, including equivalence checking, program logics, and compiler correctness to verify these quantum programs. In this talk I will survey the landscape of quantum program verification, highlight emerging approaches, and identify open problems.

This talk is designed to be accessible to a general audience; no prior background in quantum computing is expected.

Jennifer Paykin is an Assistant Professor of Computer Science at the University of Vermont, where she works at the intersection of programming languages and quantum computing. Her research focuses on designing abstractions, type systems, and tools inspired by both mathematical theory and real-world experimental constraints, often in collaboration with physicists, mathematicians, and engineers.

Before joining UVM, Dr. Paykin was a research scientist at Intel working on the formal verification and optimization of the Intel Quantum SDK. She also held a research position at Galois working on security, formal methods, and high-assurance hardware. She earned her Ph.D. from the University of Pennsylvania.