# Formal Verification of Quantum Programs: Theory, Tools and Challenges

arXiv: https://arxiv.org/abs/2110.01320 · HTML: https://mlsanity.com/paper/2110.01320/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Oct 2021.

## Built on by (most cited first, 4 of 4)

- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [Generating executable oracles to check conformance of client code to requirements of JDK Javadocs using LLMs](https://mlsanity.com/paper/2411.01789/) (2024)
- [Quantum Machine Learning in Precision Medicine and Drug Discovery -- A Game Changer for Tailored Treatments?](https://mlsanity.com/paper/2502.18639/) (2025)
- [QEncodeBench: Can Large Language Models Encode Classical Problems into Verified Quantum Oracles?](https://mlsanity.com/paper/2609.20319/) (2026)

## Abstract (arXiv)

Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backed up by the increase of research in the field. Significant efforts are being made to improve the reliability of quantum hardware and to develop suitable software to program quantum computers. In contrast, the verification of quantum programs has received relatively less attention. Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware. Research into creating verification frameworks for quantum programs has seen recent development, with a variety of tools implemented using a collection of theoretical ideas. This survey aims to be a short introduction into the area of formal verification of quantum programs, bringing together theory and tools developed to date. Further, this survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.