Pith. sign in

REVIEW 4 major objections 5 minor 1 cited by

CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler

T0 review · 4 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A mostly-automated framework verifies 26 of Qiskit's 30 compiler passes and catches three real bugs.

desk verdict 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. read the letter →

arxiv 1908.08963 v5 pith:422YCUPE submitted 2019-08-23 quant-ph cs.ETcs.PL

Yunong Shi , Runzhou Tao , Xupeng Li , Ali Javadi-Abhari , Andrew W. Cross , Frederic T. Chong , Ronghui Gu This is my paper · ORCID
classification quant-phcs.ETcs.PL
keywords quantumcompilerverificationQiskitcircuitequivalenceSMTsolvingpasssymbolicexecutionformalcalculus
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

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.

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 (4)
  1. [§6.1–6.2] 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.
  2. [§4, 'Soundness proofs' paragraph] 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.
  3. [§6.1, loop templates] 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.
  4. [§5, 'Verified quantum data conversions'] 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.
minor comments (5)
  1. [§6.1] 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'.
  2. [§8.3] 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.
  3. [Various] 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.
  4. [§9] 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'.
  5. [§2.1 and §8.1] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: verification reduces to external calculus-soundness trust, not to its own outputs.

full rationale

The claimed derivation chain is: annotated CertiQ source -> synthesizer produces symbolic VCs and executable Python -> verifier checks VCs using quantum-circuit-calculus rules and verified-library specs -> pass is extracted and run in Qiskit. I can find no step where a conclusion is equivalent to its input by construction or where a fitted parameter is renamed as a prediction. The calculus rules are independent lemmas about matrix semantics: the paper says "The symbolic execution, rewriting rules, and the shortcut lemmas are treated as axioms in CertiQ and are proven using the denotational semantics with the Coq proof assistant." Using such rules to verify passes is a normal axiom/lemma application, not a self-definitional reduction. Real gaps exist but are not circularity: the Coq soundness proofs and shortcut lemmas are referenced but not supplied (the text points to "Appendix??"), and the synthesizer/wrapper equivalence between the symbolic program and the executable Python is not given a refinement theorem (Section 6.2). Those are trust/soundness gaps. Self-citations to the authors' prior work (e.g., [18], [19], [26]) appear only in background and are not load-bearing for the verification claims. External checks—Qiskit regression tests and bugs confirmed by the Qiskit team—provide independent validation. Since no specific equation or renamed fitting can be quoted that reduces the verification claim to its assumptions, the circularity score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central verification chain rests on several premises that the preprint does not fully prove or ship as machine-checked artifacts: the calculus rules, the synthesizer correctness, the loop templates, trusted external functions, and the SMT solver. All are reasonable as trust bases, but they remain axioms in the published text.

assumptions (5)
  • domain assumption The quantum circuit calculus rewriting rules (SWAP, cancellation, commutation, bridging) are sound with respect to denotational semantics.
    CertiQ states these rules are 'treated as axioms in CertiQ' and refers to Coq soundness proofs that are not included in the preprint (§4).
  • ad hoc to paper The CertiQ synthesizer preserves the semantics of the source program when generating both the symbolic representation and the executable Python code.
    Section 6.2 describes code generation but does not prove the generated reachable code is semantically equal to the verified symbolic representation.
  • ad hoc to paper The three pre-defined loop templates (iterate_all_gates, while_gate_remaining, collect_runs) correctly encode the loop semantics, including base cases and invariants.
    Section 6.1 introduces templates with pre-defined invariants, but the paper does not demonstrate that the templates exactly match arbitrary Python loop execution.
  • domain assumption Python lists and other trusted library components are correctly implemented, and external functions satisfy their user-specified contracts.
    The paper replaces Qiskit DAG with list-based circuits 'with appropriate assumptions that Python lists are correctly implemented' (§5), and external functions are explicitly put into the TCB (§6.1).
  • domain assumption The Z3 SMT solver is sound for the theory of arrays and uninterpreted functions used in the verification conditions.
    The verifier invokes Z3 to decide satisfiability; the soundness of the overall framework depends on the solver's soundness, which is standard but unstated as a formal axiom.

how reviews work

0 comments
Cite this review

Pith. "Pith review of CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler." pith.science (2026). https://pith.science/paper/422YCUPE

@misc{pith2026190808963,
  author       = {Pith},
  title        = {Pith review of: CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/422YCUPE}},
  note         = {Machine review of arXiv:1908.08963}
}
read the original abstract

We present CertiQ, a verification framework for writing and verifying compiler passes of Qiskit, the most widely-used quantum compiler. To our knowledge, CertiQ is the first effort enabling the verification of real-world quantum compiler passes in a mostly-automated manner. Compiler passes written in the CertiQ interface with annotations can be used to generate verification conditions, as well as the executable code that can be integrated into Qiskit. CertiQ introduces the quantum circuit calculus to enable the efficient checking of equivalence of quantum circuits by encoding such a checking procedure into an SMT problem. CertiQ also provides a verified library of widely-used data structures, transformation functions for circuits, and conversion functions for different quantum data representations. This verified library not only enables modular verification but also sheds light on future quantum compiler design. We have re-implemented and verified 26 (out of 30) Qiskit compiler passes in CertiQ, during which three bugs are detected in the Qiskit implementation. Our verified compiler pass implementations passed all of Qiskit's regression tests without showing noticeable performance loss.

Figures

Figures reproduced from arXiv: 1908.08963 by the authors.

Figure 1
Figure 1. Circuit diagram symbols (top) and denotational se￾mantics (bottom) for several 1-qubit and 2-qubit gates. CertiQ, two of which are specific to quantum soft￾ware. 2 Background In this section, we introduce the necessary background on the verification of quantum computing and quantum compilation. 2.1 Quantum Data and Representations The ability to convert quantum data between different representations provides great f… view at source ↗
Figure 3
Figure 3. An example of circuit transformation made by looka￾head swap, one of routing passes. The first gate in circuit (b) is a quantum swap gate, which swaps the quantum state of the two connected qubits. Consequently, all the following gates operating on these two qubits have to swap the two operands. the combination of single qubit rotations. Usually, ro￾tations on the Bloch sphere in quantum compilers are implemented by… view at source ↗
Figure 4
Figure 4. shows the workflow of verifying a compiler pass written in CertiQ. In the rest of this section, we will fake a dummy compiler pass as a running example [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figures from the paper (6 more)
Figure 5
Figure 5. Figure 5: Denotational semantics of quantum circuits and uni￾tary operations in CertiQ. matrix denotes the unitary ma￾trices of the quantum operations. where nqreg is the number of qubits in the quantum reg￾ister used in the circuit. For example, the denotational semantics of an…
Figure 6
Figure 6. Figure 6: Examples of rules for reducing and rewriting gates. They are bridging rules (above), cancellation rules (2nd line), commutativity rules (3rd, 4th line), and swap rules (bottom). The cancellation rules applying two adjacent 𝐶𝑋 gates on the same pair of qubits will not c…
Figure 7
Figure 7. Figure 7: The simulation diagram defines the condition in which data representations can be converted safely. Take the conversion between the Bloch sphere rep￾resentation and the qubit state vector representation as an example. For single qubit optimizations, IRs of qubits (and …
Figure 8
Figure 8. Figure 8: Correct execution (top) and incorrect execution (bot￾tom) of merge_1q_gate. 8.2 commutation passes commutation_analysis and commutative_cancellation are a pair of compiler passes that optimize Qiskit DAG￾Circuits using the quantum commutation rules and the cancellation…
Figure 9
Figure 9. Figure 9: A working example of commutation_analysis and commutative_cancellation. (a) The un-optimized cir￾cuit, (b) commutation_analysis forming the commutation groups, and (c) commutative_cancellation cancels self￾inverse gates inside groups. We find two bugs when re-implement…
Figure 10
Figure 10. Figure 10: (left) A counter-example generated by CertiQ that shows Qiskit’s lookahead_swap pass does not always termi￾nate on the IBM 16 qubit device. (right) The coupling map of the IBM 16 qubit device. Arrows indicate available CNOT directions (which does not affect the swap i…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. An experience-based classification of quantum bugs in quantum software

    quant-ph 2025-09 conditional novelty 5.0 of 10

    A largely experience-based catalog of 14 quantum software bugs proposes an intersection-aware classification and finds no one debugging strategy maps cleanly onto bug classes.

Reference graph

Works this paper leans on

30 extracted references · 28 canonical work pages · cited by 1 Pith paper

  1. [1]

    Towards Large-scale Functional Verification of Universal Quantum Circuits

    Matthew Amy. Towards Large-scale Functional Verification of Universal Quantum Circuits. Electronic Proceedings in Theoretical Computer Science, 287:1–21, jan 2019

    work page 2019

  2. [2]

    Matthew Amy, Martin Roetteler, and Krysta M. Svore. Ver- ified Compilation of Space-Efficient Reversible Circuits. In Computer Aided Verification, pages 3–21. International Con- ference on Computer Aided Verification, 2017

    work page 2017

  3. [3]

    Nuclear Induction.Phys

    F Bloch. Nuclear Induction.Phys. Rev., 70(7-8):460–474, oct 1946

    work page 1946

  4. [4]

    Equivalent Quantum Circuits

    Juan Carlos Garcia-Escartin and Pedro Chamorro-Posada. Equivalent Quantum Circuits. Technical report, Universidad de Valladolid, Dpto. Teoria de la Senal e Ing., 2011

    work page 2011

  5. [5]

    Available electronically athttp: //coq.inria.fr/doc

    The Coq Development Team.The Coq Reference Manual, version 8.4, August 2012. Available electronically athttp: //coq.inria.fr/doc

    work page 2012

  6. [6]

    Open quantum assembly language.arXiv preprint arXiv:1707.03429, 2017

    Andrew W Cross, Lev S Bishop, John A Smolin, and Jay M Gambetta. Open quantum assembly language.arXiv preprint arXiv:1707.03429, 2017

    arXiv 2017

  7. [7]

    Z3: An efficient SMT Solver

    Leonardo DeMoura andNikolaj Bjørner. Z3: An efficient SMT Solver. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 LNCS, pages 337–340, 2008

    work page 2008

  8. [8]

    Cambridge University Press, 2009

    Philippe Gille and Tamas Szamuely.Central Simple Algebras and Galois Cohomology. Cambridge University Press, 2009

    work page 2009

Show all 30 references
  1. [9]

    Verified Optimization in a Quantum Intermediate Representation.arxiv, apr 2019

    Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. Verified Optimization in a Quantum Intermediate Representation.arxiv, apr 2019. 11

    2019

  2. [10]

    LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation

    Chris Lattner and Vikram Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. Technical report, UIUC, 2003

    2003

  3. [11]

    Formal verification of a realistic compiler.Com- munications of the ACM, 52(7):107–115, 2009

    Xavier Leroy. Formal verification of a realistic compiler.Com- munications of the ACM, 52(7):107–115, 2009

    2009

  4. [12]

    Q| SI?: A quantum programming environment

    Shusen Liu, Xin Wang, Li Zhou, Ji Guan, Yinan Li, Yang He, Runyao Duan, and Mingsheng Ying. Q| SI?: A quantum programming environment. InLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intel- ligence and Lecture Notes in Bioinformatics), volu...

    2018

  5. [13]

    Lopes, David Menendez, Santosh Nagarakatte, and John Regehr

    Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. Provably correct peephole optimizations with alive. InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’15, page 22–32, New York, NY, USA, 2015. Associati...

    2015

  6. [14]

    Forward and backward simulations

    Nancy Lynch and Frits Vaandrager. Forward and backward simulations. Information and Computation, 121(2):214–233, 1995

    1995

  7. [15]

    Quantum Circuit Simplification and Level Compaction.IEEE Transactions on Computer-Aided Design of Integrated Cir- cuits and Systems, 27(3):436–444, mar 2008

    D Maslov, G W Dueck, D M Miller, and C Negrevergne. Quantum Circuit Simplification and Level Compaction.IEEE Transactions on Computer-Aided Design of Integrated Cir- cuits and Systems, 27(3):436–444, mar 2008

    2008

  8. [16]

    McKay, Thomas Alexander, Luciano Bello, Michael J

    David C. McKay, Thomas Alexander, Luciano Bello, Michael J. Biercuk, Lev Bishop, Jiayin Chen, Jerry M. Chow, AntonioD. Córcoles, DanielEgger, StefanFilipp, JuanGomez, Michael Hush, Ali Javadi-Abhari, Diego Moreda, Paul Na- tion, Brent Paulovicks, Erick Winston, Christopher J. ...

    2018

  9. [18]

    Baker, Ali Javadi-Abhari, Fred- eric T

    Prakash Murali, Jonathan M. Baker, Ali Javadi-Abhari, Fred- eric T. Chong, and Margaret Martonosi. Noise-Adaptive Compiler Mappings for Noisy Intermediate-Scale Quantum Computers. pages 1015–1029. Association for Computing Machinery (ACM), 2019

    2019

  10. [19]

    Mckay, Margaret Martonosi, and Ali Javadi-Abhari

    Prakash Murali, David C. Mckay, Margaret Martonosi, and Ali Javadi-Abhari. Software mitigation of crosstalk on noisy intermediate-scale quantum computers. In Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operati...

    2020

  11. [20]

    Scaling symbolic evaluation for automated verification of systems code with serval

    Luke Nelson, JamesBornholt, Ronghui Gu, AndrewBaumann, Emina Torlak, and Xi Wang. Scaling symbolic evaluation for automated verification of systems code with serval. InPro- ceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP ’19, pages 225–242, New York, NY, USA,

  12. [21]

    Hyperkernel: Push-button verification of an os kernel

    Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dy- lan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-button verification of an os kernel. In Proceedings of the 26th Symposium on Operating Systems Principles, SOSP ’17, pages 252–269, New York, NY, USA,

  13. [22]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang.Quantum Compu- tation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, New York, NY, USA, 10th edi- tion, 2011

    2011

  14. [23]

    Available at https://github.com/ Qiskit/qiskit-terra/issues/1871

    Qiskit bug report, 2018. Available at https://github.com/ Qiskit/qiskit-terra/issues/1871

    2018

  15. [24]

    ReQWIRE: Reasoning about Reversible Quantum Circuits

    Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic. ReQWIRE: Reasoning about Reversible Quantum Circuits. arXiv e-prints, page arXiv:1901.10118, Jan 2019

    1901 arXiv

  16. [25]

    QWIRE Practice: Formal Verification of Quantum Circuits in Coq

    Robert Rand, Jennifer Paykin, and Steve Zdancewic. QWIRE Practice: Formal Verification of Quantum Circuits in Coq. Electronic Proceedings in Theoretical Computer Science, 2018

    2018

  17. [26]

    Schuster, Henry Hoffmann, and Frederic T

    Yunong Shi, Nelson Leung, Pranav Gokhale, Zane Rossi, David I. Schuster, Henry Hoffmann, and Frederic T. Chong. Optimized Compilation of Aggregated Instructions for Real- istic Quantum Computers. InASPLOS, Providence, Rhode Island, 2019

    2019

  18. [27]

    Push-Button Verification of File Systems via Crash Refinement

    Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button Verification of File Systems via Crash Refinement. In the Proceedings of the 12th USENIX Sym- posium on Operating Systems Design and Implementation (OSDI, 2016

    2016

  19. [28]

    Verified translation between low-level quantum languages

    Kartik Singhal, Robert Rand, and Michael Hicks. Verified translation between low-level quantum languages. The First International Workshop on Programming Languages for Quan- tum Computing, jan 2020

    2020

  20. [29]

    Available at https: //github.com/Qiskit/qiskit-terra/issues

    Qiskit Terra Github issue page, 2018. Available at https: //github.com/Qiskit/qiskit-terra/issues

    2018

  21. [30]

    Viamontes, Igor L

    George F. Viamontes, Igor L. Markov, and John P. Hayes. Checking equivalence of quantum circuits and states. In Georges G E Gielen, editor,ICCAD. IEEE, 2007

    2007

  22. [31]

    Floyd–hoare logic for quantum programs

    Mingsheng Ying. Floyd–hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems, 33(6):1–49, dec 2011. 12

    2011

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.