[Submitted on 9 Aug 2026]
Title:VQ System Design: Connecting Quantum Programs, Proofs, and Resource Reports
Abstract: Quantum-algorithm evidence often assigns functional correctness, success probability, and resource cost to artifacts produced by separate tools. VQ addresses that provenance problem in Lean 4 by defining circuits and hybrid programs as authoritative syntax, proving behavior over that syntax, and deriving logical resource reports from it. This note specifies VQ's design goals, architectural layers, trust boundary, symbolic strategy for circuit families, and resource and probability endpoints. It also records the current limits: terminal hybrid-program distributions and most circuit-to-complex approximation results remain test-local, reports stop at logical gates and dependency depth, and the Lean-native VECDSA game lacks an external hostile-submission adapter.
| Subjects: | Programming Languages (cs.PL); Logic in Computer Science (cs.LO) |
| Cite as: | marXiv:2608.00030 [cs.PL] (or marXiv:2608.00030v1 [cs.PL] for this version) |
Submission history
[v1] Sun, 9 Aug 2026 16:56:09 UTC (292 KB)