QEDIA: Quantum Program Verification in Lean
Yuanjie, Ren, Zhicheng Zhang, Junyi Liu, Jinzheng Li, Yidi Qi, Mingsheng Ying
quant-ph
Oct 13, 2026 · v1
cs.PL
TL;DR
Formalizes the quantum Hoare logic QHL+ in Lean 4 on Mathlib, proves it sound, and verifies quantum programs using an LLM-based prover agent.
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.
Problem
Quantum programs interleave classical and quantum computation, which limits testing. Formally verifying them requires mechanizing a program logic at every level, from quantum mechanics through syntax and semantics to proof rules. Such mechanizations and the program proofs built on them usually take substantial manual effort.
Approach
QEDIA is an open Lean 4 library built on Mathlib that formalizes the quantum Hoare logic QHL+. It covers state spaces, programs, execution paths, classical–quantum assertions, and the proof systems. Classical components are expressed directly as Lean functions and predicates, and quantum components are built on top of them. The library and program proofs are constructed under human supervision by an LLM-based prover agent. In that agent, a leader fixes the statements, subagents prove them, and the general-purpose core is extended with quantum-specific checks.
Results
The QHL+ proof system is proved sound in Lean for both partial and total correctness. Eleven example programs are verified for total correctness, including the quantum Fourier transform, phase estimation, repeat-until-success circuits, and Trotterized Hamiltonian simulation, some of which reuse verified subprograms.
