{"id":"5c8ca98b-9e6f-4966-a9be-d61278c09eaa","arxiv_id":"1908.08963","paper_version":5,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"CertiQ re-implements 26 Qiskit compiler passes in a verifiable interface and uses SMT-based symbolic execution to prove they preserve quantum circuit semantics, uncovering three real bugs in the original Qiskit implementation.","lead":"This paper presents CertiQ, a framework that mostly automatically verifies the correctness of compiler passes for IBM's Qiskit quantum compiler. If correct, it offers a practical, push-button way to prove that Qiskit's optimization and routing steps preserve a quantum program's behavior, addressing a real reliability gap in near-term quantum software.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The weakest link is the unproved equivalence between the CertiQ symbolic program used for verification and the executable Python/wrapper that actually runs in Qiskit.","rationale":"The reader identified the same load-bearing concern: the synthesizer and wrapper translate verified symbolic programs into executable Qiskit passes, and the paper does not establish that these translations preserve semantics. This is the right focus because the paper's headline is about verified passes running in a real compiler; if the generated code is not faithful to the verified model, the verification claim does not transfer to the code users execute. The paper has independent support: reimplementing 26 passes and finding three real Qiskit bugs is evidence that the verification approach can expose genuine issues, and passing Qiskit's regression tests shows practical integration. However, regression tests are not exhaustive, so they do not settle the translation-equivalence question. The missing appendix, unresolved references, and unshipped artifact further prevent full acceptance, but they are addressable. I agree with the CONDITIONAL verdict: make the artifact available, supply a formal refinement argument or differential-testing evidence for the synthesizer and wrapper, and complete the missing technical appendix. This is not a claim of dishonesty or a fatal flaw; it is a precise gap in the chain connecting the formal verification to the executed compiler pass.","tokens_in":15139,"tokens_out":3860,"duration_ms":43964,"concrete_test":"Release the CertiQ artifact and run a randomized differential test: for each of the 26 passes, generate 10,000 random QASM circuits (1–5 qubits, including conditional gates where supported), transpile with the original Qiskit pass and with the CertiQ-generated pass, and compare the resulting unitary matrices using Qiskit's statevector simulator. Any semantic mismatch between the two outputs would show that the synthesized executable does not match the verified pass semantics; if all 260,000 comparisons match, the wrapper/synthesizer translation receives strong empirical support.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that 26 Qiskit passes were re-implemented and verified, and that the code extracted from CertiQ is what runs in Qiskit. For this to be true, the synthesizer must be a faithful compiler: the symbolic program sent to the verifier and the executable Python passed through the DAG-to-OpenQASM-to-DAG wrapper must have the same semantics as the annotated CertiQ source. Section 6 describes the synthesizer and wrapper operationally, but gives no refinement theorem, no formal semantics for the CertiQ language, and no argument that the wrapper conversions preserve circuit equivalence in both directions. Section 6.1 explicitly places external functions in the TCB, but the synthesizer and wrapper themselves are not similarly acknowledged. The three loop templates are said to be pre-defined, yet the paper does not prove that the verification conditions generated from a template match the behavior of the generated loop in Qiskit. If any of these translations differ, a pass can be verified symbolically while the executable pass changes circuit semantics in real runs. Regression tests passing would not reliably catch this because Qiskit's tests are not exhaustive. This gap is load-bearing because it sits between the formal result and the realistic-compiler claim. The missing Appendix?? references and absent Coq soundness proofs compound this, but even a correct calculus would not transfer to certification if the emitted code differs from the verified model.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents CertiQ, a framework for mostly-automated verification of quantum compiler passes in Qiskit. Compiler passes are written in a Python-like annotated language; a synthesizer produces both a symbolic representation used to generate SMT-based verification conditions and executable Python code compatible with Qiskit. The framework introduces a quantum circuit calculus with rewriting rules, a verified library of circuit transformations and data conversions, and a verifier that encodes proof obligations into Z3 formulas. The authors report re-implementing and verifying 26 of 30 Qiskit passes, detecting three bugs in Qiskit, and confirming that the generated passes pass Qiskit's regression tests without noticeable performance loss.","tokens_in":15404,"tokens_out":2788,"duration_ms":28951,"significance":"If the central claim holds, CertiQ would be a landmark step toward practical verification of real-world quantum compilers: it would be the first mostly-automated framework to verify realistic Qiskit passes, with an SMT-based equivalence check that avoids exponential denotational reasoning and a reusable verified library. The paper also provides falsifiable, concrete results: 26 verified passes, three reported bugs, and regression-test passage. Strengths include an honest identification of external functions as part of the trusted computing base, a forward-simulation framework for data conversions, and a demonstrated use of the framework to find a non-termination bug in lookahead_swap. However, the machine-checked proofs of the calculus are not shipped, the synthesizer's correctness is not established, and several appendix references and figures are missing, so the claimed end-to-end guarantee cannot currently be checked from the manuscript alone.","major_comments":[{"comment":"The correctness of the synthesizer is load-bearing but unproven. The paper claims that CertiQ-generated code can be integrated into Qiskit and that the passes are verified, yet the verification applies to the symbolic representation, not the executable Python code produced by the synthesizer or the DAG-to-OpenQASM-to-DAG wrapper. The paper gives only an operational description of the synthesizer and wrapper and no refinement theorem, no formal semantics for the CertiQ source language, and no argument that both generated artifacts preserve the source program's semantics. A discrepancy between the verified symbolic program and the executed code would invalidate the central claim that the Qiskit passes are verified. The authors should either prove the synthesizer and wrapper correct, or explicitly place them in the trusted computing base and weaken the corresponding claims.","section":"§6.1–6.2"},{"comment":"The foundation of the verification chain is not independently checkable. The text states that the symbolic execution rules, rewriting rules, and shortcut lemmas 'are treated as axioms' and that their soundness was proven in Coq, but no Coq developments, proof artifacts, or even detailed proof sketches are provided, and the referenced Appendix appears as 'Appendix??'. Since every pass verification and every library-function verification inherits these axioms, the entire claim of 'verified' passes rests on uncheckable assumptions in the preprint. The authors should release the Coq proofs or, at a minimum, provide a complete account of the axioms and their soundness arguments in the appendix.","section":"§4, 'Soundness proofs' paragraph"},{"comment":"The three loop templates are claimed to pre-define loop invariants, but the paper does not prove that the verification conditions generated from a template correctly capture the semantics of the generated loop, including base cases and termination. In the iterate_all_gates example, the assertions constrain i but there is no explicit proof obligation for the base case that the empty circuit is equivalent to the first zero gates, and the relationship between the template's formal assertions and the actual behavior of the synthesized loop in Qiskit is not established. This gap is part of the synthesizer-correctness issue and is load-bearing for any pass whose proof relies on these templates.","section":"§6.1, loop templates"},{"comment":"The forward-simulation argument for data conversions is not fully presented. The paper refers to a simulation diagram that is missing ('as shown in??' and 'Fig. 7' are absent from the text), and the definition of the conversion relation and the proof that the listed conversions satisfy the simulation conditions are only sketched. Since the claimed detection of a severe bug in Qiskit's representation conversion depends on this argument, the missing diagram and formal details prevent the reader from verifying the conversion-soundness claim.","section":"§5, 'Verified quantum data conversions'"}],"minor_comments":[{"comment":"In the description of iterate_all_gates, the text says 'the new_circ after this iteration must be equivalent to the first i 1 gates of circ', which appears to be a typo for 'i+1 gates'.","section":"§6.1"},{"comment":"The sentence 'we find a counter-example circuit on coupling map of the IBM 16 qubit device, where the lookahead_swap pass does not terminate on' is grammatically incomplete and should be rephrased.","section":"§8.3"},{"comment":"Multiple references to 'Appendix??' and 'as shown in??' appear throughout the paper (e.g., §4 and §5); these missing references and figures should be resolved before publication.","section":"Various"},{"comment":"The evaluation would benefit from concrete experimental details: how regression tests were run, what 'no noticeable performance loss' means operationally, and what measurements support the claim about verification times finishing 'within seconds' or 'within one minute'.","section":"§9"},{"comment":"The notation for gates and the matrix representations in Table 1 contains minor typesetting issues (e.g., 'm1g−−−→' in Fig. 8) that should be corrected.","section":"§2.1 and §8.1"}],"recommendation":"major_revision","confidential_remarks":"The paper makes a strong and interesting claim, but the missing Coq artifacts and the unproven synthesizer equivalence are substantial gaps. The manuscript is not ready for acceptance, but the direction is sound and the gaps are addressable. I would encourage the authors to ship the verification artifacts, explicitly delimit the trusted computing base, and add the missing appendix content and figures."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"CertiQ is a credible step forward: it brings Alive/Yggdrasil-style push-button SMT verification to a realistic quantum compiler, and the reported bug findings — the lookahead_swap non-termination, the transitivity bug in commutation analysis, and the Bloch-sphere phase bug in optimize_1q_gate — are concrete and plausible. The symbolic circuit calculus with SMT arrays is a genuine adaptation, and the verified conversion library is a useful building block. Getting 26 of 30 Qiskit passes reimplemented and verified, and passing Qiskit's regression tests, is real evidence of engineering value.\n\nThe soft spot is load-bearing, though. Verification happens on a symbolic program produced by the CertiQ synthesizer, but the executable code that actually runs in Qiskit goes through a DAG-to-OpenQASM-to-DAG wrapper. The paper gives no refinement theorem, no formal semantics for the CertiQ language, and no argument that the wrapper conversions preserve circuit equivalence. If the synthesizer or the wrapper changes semantics, a pass can be verified symbolically while the deployed code is wrong. That is not a minor gap; it sits exactly between the formal result and the 'realistic compiler' claim.\n\nAlso, the quantum circuit calculus rules are 'treated as axioms' in CertiQ; the paper says soundness proofs were done in Coq, but no Coq outputs are shipped, and the appendix has unresolved '??' references. The loop templates' base cases are not explicit. These are addressable omissions, but the trust chain in the preprint is incomplete.\n\nThe stress-test concern about synthesizer equivalence lands. Still, this is not a takedown — the approach is promising, and the bugs found are evidence that the method has practical value. The paper just overstates what is currently checked.\n\nAudience: quantum compiler developers and formal methods folks. It deserves peer review; a serious editor should send it to referees. But the reviewers should insist on the artifact, the Coq proofs, and a clear argument for synthesizer correctness. Without those, the headline claim of verified Qiskit passes is not substantiated.\n\nFor your own work, I'd wait for a version with artifacts before citing the verification claim.","headline":"Promising push-button verification for Qiskit passes with real bug findings, but the missing artifact and unproven synthesizer/wrapper equivalence keep the headline claim from being fully substantiated.","tokens_in":15926,"tokens_out":3186,"would_cite":true,"duration_ms":31029,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A mostly-automated framework verifies 26 of Qiskit's 30 compiler passes and catches three real bugs.","keywords":["quantum compiler verification","Qiskit","quantum circuit equivalence","SMT solving","compiler pass verification","symbolic execution","formal verification","quantum circuit calculus"],"falsifier":"Feed a randomly generated Qiskit circuit through one of the 26 CertiQ-generated passes and compare input and output circuits with a full state-vector simulator; any unitary mismatch would show the generated executable diverges from the verified symbolics, refuting the claim.","tokens_in":14921,"feed_emoji":"⚛️","tokens_out":9188,"duration_ms":79945,"temperature":0.7,"pith_summary":"CertiQ sets out to show that formal verification can be brought to a production quantum compiler: a programmer writes a compiler pass once in a Python-like annotated interface, and the framework automatically generates both executable code for Qiskit and verification conditions that a satisfiability-modulo-theories (SMT) solver can check. Its strategy is to avoid exponential matrix semantics and instead prove circuit equivalence symbolically, using a small set of sound rewriting rules and a verified library of circuit transformations and data conversions. If the approach works, quantum compiler bugs can be caught at development time rather than through noisy hardware runs or unscalable simulation. The paper reports that it does work: 26 of Qiskit's 30 passes were re-implemented and verified, all passed Qiskit's regression tests with no noticeable performance loss, and three bugs in Qiskit's own implementation were found.","feed_headline":"Automated verifier proves 26 of Qiskit's 30 passes correct","feed_subtitle":"It checks circuit rewriting meaning with an SMT solver and found three bugs in Qiskit itself.","key_machinery":"The quantum circuit calculus is the mechanism that carries the argument. It represents a circuit as a symbolic expression $app(C,Q)$ that applies $C$ to a register of symbolic qubits, with rewriting rules—adjacent CNOT cancellation, SWAP argument exchange, gate commutation, and similar local identities—whose soundness is proven once against the matrix semantics in an interactive proof assistant. When a pass is written in CertiQ, the synthesizer expands branches, abstracts loops through provided templates, and turns the symbolic execution into proof obligations of the form $P_1 \\wedge P_2 \\wedge \\neg G$; an SMT solver checks unsatisfiability, so a satisfying assignment would be a counterexample. A verified library of transformation functions and forward-simulation-based conversion functions supplies the reusable lemmas that keep most verifications within seconds.","core_discovery":"CertiQ's central claim is that real-world quantum compiler passes can be verified mostly automatically by reducing each pass to a semantic-preservation check over symbolic circuits and encoding that check as an SMT satisfiability problem. The framework contributes a quantum circuit calculus whose symbolic execution and gate rewriting rules allow adjacent gates to be cancelled, commuted, or swapped without constructing unitary matrices, plus a verified library of high-level transformations and representation conversions that make proofs modular. Using these components, the authors re-implement and verify 26 of the 30 passes in Qiskit version 0.192, integrate the generated code into Qiskit through a wrapper that converts the circuit's directed-acyclic-graph representation to the textual intermediate representation and back, and report that every generated pass passes Qiskit's regression tests. The verification process also identifies three bugs in the original Qiskit implementation, including a routing pass (lookahead_swap) that can fail to terminate on a 16-qubit coupling map.","pith_inferences":["The same recipe should transfer to other quantum compilers whose passes manipulate circuit intermediate representations, since the circuit calculus and the simulation-diagram criterion are not tied to Qiskit's specific data structures.","The non-termination bug suggests that monotonic-function termination checks, as CertiQ uses, are worth adding to routing passes generally, especially as hardware coupling maps grow and greedy heuristics get more complicated.","CertiQ's explicit refusal to convert Bloch-sphere representations beyond one qubit implies that any future verified optimizer wanting multi-qubit phase information will need a representation that tracks global phases, not just the Bloch projection.","The framework's guarantee is compositional rather than absolute: each external function is trusted by specification, so integrating CertiQ with more powerful third-party libraries will require those specifications to be verified or narrowed."],"forward_implications":["Qiskit's transformation passes can be checked for semantic preservation and termination without constructing full unitary matrices, making verification practical on circuits of any size.","Verified passes can be dropped into Qiskit directly because CertiQ generates both the proof and the executable code from one source, and the generated code passes Qiskit's own regression tests.","The verified library of circuit transformations and representation conversions can be reused to verify future passes with little more than loop and external-function annotations.","Because three real bugs were found—including a non-terminating routing pass—automatic verification of this kind can act as a practical bug-finding tool for quantum compilers."],"supporting_citations":[{"why":"Supplies the push-button SMT-based model for verifying compiler optimizations that CertiQ adapts to quantum circuits.","marker":"[13]"},{"why":"Supplies the proof-obligation workflow and the idea of generating verification conditions automatically from code.","marker":"[27]"},{"why":"Provides the SMT engine that discharges CertiQ's verification conditions.","marker":"[7]"},{"why":"Defines the simulation-diagram criterion CertiQ uses to prove data-representation conversions sound.","marker":"[14]"},{"why":"Provides the interactive proof assistant in which CertiQ proves the circuit-calculus rules sound.","marker":"[5]"},{"why":"Defines the intermediate-representation syntax that CertiQ's circuit semantics and DAG conversion follow.","marker":"[6]"},{"why":"Demonstrates that a realistic compiler can be formally verified end to end, the precedent CertiQ extends to quantum compilation.","marker":"[11]"},{"why":"Prior verified compilation of reversible circuits that CertiQ contrasts with for its limited scope.","marker":"[2]"},{"why":"Prior verified optimization of a quantum intermediate representation showing the manual-proof bottleneck CertiQ automates.","marker":"[9]"},{"why":"Prior verified translation between low-level quantum languages whose manual proof burden CertiQ aims to remove.","marker":"[28]"}],"fun_headline_variants":["CertiQ verifies 26 Qiskit passes, catches 3 bugs","SMT-based tool certifies 26 of Qiskit's passes","Mostly-automatic verification of quantum compiler passes","CertiQ: Nearly all Qiskit passes formally verified","Three bugs found in Qiskit by automated verifier"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The guarantee is only as strong as the assumption that the executable Python code CertiQ generates and wires into Qiskit behaves exactly like the symbolic circuit program that was verified, and that every user-declared external function specification is faithful.","fun_headline_variants_meta":{"raw":{"variants":["CertiQ verifies 26 Qiskit passes, catches 3 bugs","SMT-based tool certifies 26 of Qiskit's passes","Mostly-automatic verification of quantum compiler passes","CertiQ: Nearly all Qiskit passes formally verified","Three bugs found in Qiskit by automated verifier"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000582,"raw_usage":{"total_tokens":2738,"prompt_tokens":945,"completion_tokens":1793,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":561,"completion_tokens_details":{"reasoning_tokens":1705}},"tokens_in":561,"tokens_out":1793,"duration_ms":13888,"temperature":1.0,"reasoning_tokens":1705,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:25:12.885755+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Feed a randomly generated Qiskit circuit through one of the 26 CertiQ-generated passes and compare input and output circuits with a full state-vector simulator; any unitary mismatch would show the generated executable diverges from the verified symbolics, refuting the claim.","supporting_citations":[{"cited_title":"Lopes, David Menendez, Santosh Nagarakatte, and John Regehr","cited_arxiv_id":null,"evidence_quote":"Supplies the push-button SMT-based model for verifying compiler optimizations that CertiQ adapts to quantum circuits."},{"cited_title":"Push-Button Verification of File Systems via Crash Refinement","cited_arxiv_id":null,"evidence_quote":"Supplies the proof-obligation workflow and the idea of generating verification conditions automatically from code."},{"cited_title":"Z3: An efficient SMT Solver","cited_arxiv_id":null,"evidence_quote":"Provides the SMT engine that discharges CertiQ's verification conditions."},{"cited_title":"Forward and backward simulations","cited_arxiv_id":null,"evidence_quote":"Defines the simulation-diagram criterion CertiQ uses to prove data-representation conversions sound."},{"cited_title":"Available electronically athttp: //coq.inria.fr/doc","cited_arxiv_id":null,"evidence_quote":"Provides the interactive proof assistant in which CertiQ proves the circuit-calculus rules sound."},{"cited_title":"Formal verification of a realistic compiler.Com- munications of the ACM, 52(7):107–115, 2009","cited_arxiv_id":null,"evidence_quote":"Demonstrates that a realistic compiler can be formally verified end to end, the precedent CertiQ extends to quantum compilation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Prior verified compilation of reversible circuits that CertiQ contrasts with for its limited scope."},{"cited_title":"Verified Optimization in a Quantum Intermediate Representation.arxiv, apr 2019","cited_arxiv_id":null,"evidence_quote":"Prior verified optimization of a quantum intermediate representation showing the manual-proof bottleneck CertiQ automates."},{"cited_title":"Verified translation between low-level quantum languages","cited_arxiv_id":null,"evidence_quote":"Prior verified translation between low-level quantum languages whose manual proof burden CertiQ aims to remove."}],"review_version":1}