[Submitted on 26 Aug 2026 (v1), last revised 21 Sep 2026 (this version, v17)]
Title:VQ: Quantum Algorithm Development and Verification with an Evolving Knowledge Base
Abstract: VQ is a Lean-based system for developing and verifying quantum algorithms, with a current focus on elliptic-curve arithmetic and the elliptic-curve discrete logarithm problem. It connects algorithm constructions, formal proofs, resource analysis, and reusable research knowledge in one repository. Its two goals are to improve algorithms and to improve the knowledge used to develop them. The algorithm library provides exact semantics, specifications for reversible and measured components, composition theorems, and logical-resource accounting for the generated programs. It retains alternative constructions with their input, workspace, and preservation conditions. The knowledge base links declarations to applicability, methods, skills, references, and research questions. Experiment records supply evidence for revisions to both collections. Checked results include complete secp256k1 point addition, ECDLP recovery probability greater than 99 percent, and resource, lookup, decoder, and Euclidean schedule bounds. A comparison of squaring components illustrates the connection between the formal library and reusable knowledge. The report compares VQ with systems for quantum programming, verification, circuit optimization, resource analysis, and proof retrieval.
| Comments: | 12 pages, 5 tables |
| Subjects: | Logic in Computer Science (cs.LO); Programming Languages (cs.PL) |
| Cite as: | marXiv:2608.00049 [cs.LO] (or marXiv:2608.00049v17 [cs.LO] for this version) |
Submission history
[v1] Wed, 26 Aug 2026 13:39:48 UTC (431 KB)
[v2] Wed, 26 Aug 2026 14:17:59 UTC (459 KB)
[v3] Sun, 30 Aug 2026 13:57:41 UTC (459 KB)
[v4] Sun, 30 Aug 2026 14:30:36 UTC (459 KB)
[v5] Sun, 30 Aug 2026 14:44:51 UTC (459 KB)
[v6] Sun, 30 Aug 2026 14:51:28 UTC (459 KB)
[v7] Sun, 30 Aug 2026 15:01:34 UTC (458 KB)
[v8] Mon, 21 Sep 2026 14:47:21 UTC (306 KB)
[v9] Mon, 21 Sep 2026 14:55:13 UTC (307 KB)
[v10] Mon, 21 Sep 2026 15:00:59 UTC (307 KB)
[v11] Mon, 21 Sep 2026 15:05:50 UTC (307 KB)
[v12] Mon, 21 Sep 2026 15:46:35 UTC (279 KB)
[v13] Mon, 21 Sep 2026 15:53:52 UTC (279 KB)
[v14] Mon, 21 Sep 2026 16:16:59 UTC (323 KB)
[v15] Mon, 21 Sep 2026 16:25:28 UTC (324 KB)
[v16] Mon, 21 Sep 2026 16:57:39 UTC (325 KB)
[v17] Mon, 21 Sep 2026 17:49:11 UTC (326 KB)
Named by
- marXiv:2609.00016
- Gives the construction and checked resource bounds for the 1601-qubit complete point-adder summarized in the VQ system report.