QEDIA: Quantum Program Verification in Lean
Abstract
Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classical computation that follows. Formal verification of such programs in a proof assistant requires mechanizing a program logic that handles this interplay consistently at every level, from the mathematics of quantum mechanics, through program syntax and semantics, to specifications and proof rules. Such mechanizations, along with the program proofs built on them, typically require substantial manual effort. We present QEDIA, a framework for verifying quantum programs with classical variables in Lean 4. At its foundation is an open library that formalizes the quantum Hoare logic QHL+ across all these levels and proves the logic sound for both partial and total correctness. We construct the library and the program proofs, under human supervision, using an LLM-based prover agent, whose general-purpose core we extend for quantum program verification. We illustrate QEDIA with verified programs including the quantum Fourier transform, phase estimation, repeat-until-success circuits, and Hamiltonian simulation.
Related
- Exact Madelung and Bohm Quantum Potential Identities in Core Lean 4 (Zero Mathlib Dependencies)
- Quantum Cryptography and Autoformalization in Lean
- QECert: Formal Foundations for Quantum Error-Correction Theory in Lean
- Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust
- Secure Quantum Handshakes: Quantum Network Verification Via Simon's Algorithm
BibTeX
@misc{yuanjie2026qedia,
title = {{QEDIA: Quantum Program Verification in Lean}},
author = {Yuanjie and Ren and Zhicheng Zhang and Junyi Liu and Jinzheng Li and Yidi Qi and Mingsheng Ying},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.17708},
eprint = {2610.17708},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.17708},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - QEDIA: Quantum Program Verification in Lean
AU - Yuanjie
AU - Ren
AU - Zhicheng Zhang
AU - Junyi Liu
AU - Jinzheng Li
AU - Yidi Qi
AU - Mingsheng Ying
PY - 2026
DA - 2026/10/13
PB - arXiv
DO - 10.48550/arxiv.2610.17708
UR - https://arxiv.org/abs/2610.17708
AB - Practical quantum programs interleave quantum and classical computation: classical data shape the quantum operations that are performed, and measurement outcomes shape the classical computation that follows. Formal verification of such programs in a proof assistant requires mechanizing a program logic that handles this interplay consistently at every level, from the mathematics of quantum mechanics, through program syntax and semantics, to specifications and proof rules. Such mechanizations, along with the program proofs built on them, typically require substantial manual effort. We present QEDIA, a framework for verifying quantum programs with classical variables in Lean 4. At its foundation is an open library that formalizes the quantum Hoare logic QHL+ across all these levels and proves the logic sound for both partial and total correctness. We construct the library and the program proofs, under human supervision, using an LLM-based prover agent, whose general-purpose core we extend for quantum program verification. We illustrate QEDIA with verified programs including the quantum Fourier transform, phase estimation, repeat-until-success circuits, and Hamiltonian simulation.
ER -