Title:VQ Among Machine-Checked Quantum Program Systems

Abstract: Quantum-program verification systems check different semantic, compilation, resource, and application claims. The survey records the checked claims used in the comparison and the program class that each claim covers. VQ combines Lean 4 syntax for unitary circuits, reversible circuits, and hybrid quantum–classical programs with exact semantics and syntax-derived resource reports. The comparison covers VQ, QWIRE, SQIR/VOQC, Qbricks, CoqQ, Qafny, qrhl-tool, and QBlue under separate criteria for semantics, program logic, compilation, equivalence, resources, mixed-state models, execution, and applications. SQIR/VOQC and Qbricks verify optimization or end-to-end algorithm results. CoqQ and qrhl-tool provide general program logics, Qafny provides automated program verification, and QBlue verifies Hamiltonian compilation. VQ proves exact semantics for an affine point-addition branch where a nonzero table address selects a finite precomputed point to add to a finite point in the target register with a different x-coordinate. It proves that a measured component restores ancillas independently of its measurement record, and that a generated binary-Euclidean schedule has width 758. Its general program logic, end-to-end algorithm success probability, approximation, and external execution coverage remain limited.

Submission history

[v1] Sun, 16 Aug 2026 21:59:27 UTC (331 KB)

[v2] Sun, 16 Aug 2026 22:12:13 UTC (378 KB)

[v3] Sun, 16 Aug 2026 22:17:16 UTC (378 KB)

[v4] Sun, 16 Aug 2026 22:26:01 UTC (379 KB)

[v5] Sun, 16 Aug 2026 22:35:38 UTC (379 KB)

[v6] Sun, 30 Aug 2026 13:57:41 UTC (376 KB)

[v7] Sun, 30 Aug 2026 14:07:29 UTC (377 KB)

[v8] Sun, 30 Aug 2026 14:51:27 UTC (377 KB)

[v9] Sun, 30 Aug 2026 15:15:51 UTC (377 KB)

[v10] Sun, 30 Aug 2026 15:19:45 UTC (377 KB)

Full text and citation

View PDF · Export BibTeX citation