https://www.mdu.se/

Quantum technology is advancing at an exceptional pace and holds the potential to transform numerous sectors on both national and global scales. As quantum systems become more sophisticated and widespread, ensuring their correctness becomes critically important. This highlights the pressing need for rigorous tools capable of analyzing and verifying their behavior. However, developing such verification tools poses significant challenges. Fundamental quantum phenomena—most notably superposition and entanglement—lead to program behaviors that differ radically from those in classical computing. These characteristics give rise to inherently probabilistic models and result in exponentially large state spaces, even for systems of modest complexity. In this paper, we outline initial steps toward addressing these challenges by drawing on insights gained from the verification of classical systems within our community. We then present a roadmap for designing novel verification frameworks that adapt the strengths of classical methods—such as succinct property specification, precise fault detection, automation, and scalability—to the quantum setting.