pith. sign in

arxiv: 2311.11571 · v4 · submitted 2023-11-20 · 💻 cs.PL · quant-ph

VyZX: Formal Verification of a Graphical Quantum Language

Adrian Lehmann , Ben Caldwell , Bhakti Shah , William Spencer , Robert Rand This is my paper

Pith reviewed 2026-05-24 06:18 UTC · model grok-4.3

classification 💻 cs.PL quant-ph
keywords formal verificationZX-calculusgraphical languagesproof assistantsquantum computationinductive definitionscategory theory
0
0 comments X

The pith

Inductive graphs from category theory enable formal proofs of ZX-calculus soundness in proof assistants.

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

VyZX supplies a library that defines graphical languages inductively so that proof assistants can verify their rewrite rules. The approach is demonstrated on the ZX-calculus by showing that its diagrammatic rewrites preserve the intended quantum semantics. The same inductive structure supports routine application of the rules inside an existing proof assistant. A visualizer is included so that diagrams can be inspected and manipulated during proof development.

Core claim

Inductive graphs derived from category-theoretic definitions of the ZX-calculus can be used inside a proof assistant to establish the soundness of its rewrite rules, thereby allowing standard inductive proof techniques to be applied to the equational theory of the graphical language without losing its diagrammatic character.

What carries the argument

Inductive graphs in VyZX, constructed from category-theoretic definitions, that represent ZX diagrams and support equational reasoning.

If this is right

  • Soundness of ZX rewrite rules is established by induction on the graph structure.
  • ZX diagrams and their rewrites become subject to the same proof techniques used for ordinary inductive datatypes.
  • An IDE visualizer allows direct graphical manipulation while the underlying proof remains inductive.
  • The same library structure can be reused for other inductively presented graphical languages.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The technique may transfer to graphical languages used in other domains such as string diagrams for monoidal categories.
  • Integration with existing quantum-circuit verifiers could allow mixed graphical and circuit-level proofs.
  • Automated tactics that operate directly on the inductive graphs could reduce manual proof effort for large diagrams.

Load-bearing premise

The inductive definitions obtained from category theory match the equational theory of the graphical language exactly, neither adding nor omitting any rewrite equivalences.

What would settle it

A concrete pair of ZX diagrams that are provably equivalent under the standard graphical semantics but not equivalent (or vice versa) under the inductive encoding would falsify the claim.

Figures

Figures reproduced from arXiv: 2311.11571 by Adrian Lehmann, Ben Caldwell, Bhakti Shah, Robert Rand, William Spencer.

Figure 1
Figure 1. Figure 1: A simple graphical program, corresponding to a CNOT in the ZX-calculus. How do we formally verify a graphical language? Of special interest are graphical languages which follow the principle that only connectivity mat￾ters [Coecke and Kissinger 2017]: We care about the connections in a graph, not the position of any given node [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A CNOT adjusted for ordering. We use these insights to present a formally verified ZX-calculus library called VyZX. By verified, we mean that all the rules pertaining to both con￾nectivity and quantum operations have been proven sound with respect to the linear-algebraic semantics of ZX-diagrams. Besides the central contribution of representing graphical structures in￾ductively, endowing them with semantic… view at source ↗
Figure 3
Figure 3. Figure 3: Z and X spiders with their standard bra-ket semantics. Fundamentally, ZX-diagrams are graphs with green and red nodes2 , called Z and X spiders, with 𝑛 inputs and 𝑚 outputs, along with a rotation angle 𝛼 ∈ [0, 2𝜋). Spiders without an explicit rotation parameter are considered to have a 0 rotation. The semantics of Z and X spiders are shown in [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Only connectivity matters: Two equal ZX-diagrams, where the [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Rules of the ZX-calculus, where 𝛼, 𝛽 ∈ R, 𝑐 ∈ N One of the most critical ZX-calculus rules is that spiders connected by an arbitrary (non-zero) number of edges can be fused into a single node with the angles added together. This rule is shown in Figure 5f. The reverse is also true: any spider can be split such that the two new spiders add up to the original angle. A corollary of this is that spiders with 0… view at source ↗
Figure 6
Figure 6. Figure 6: Common gates represented in the ZX-calculus. [PITH_FULL_IMAGE:figures/full_fig_p005_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The pentagon and triangle coherence axioms. [PITH_FULL_IMAGE:figures/full_fig_p006_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: The diagrammatic construction for monoidal category definitions, where [PITH_FULL_IMAGE:figures/full_fig_p007_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: The diagrammatic interpretations for symmetric and autonomous categories. [PITH_FULL_IMAGE:figures/full_fig_p007_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: The connection information for the hexagon isomorphism; see [PITH_FULL_IMAGE:figures/full_fig_p009_10.png] view at source ↗
Figure 12
Figure 12. Figure 12: The inductive constructors for block representation ZX-diagrams [PITH_FULL_IMAGE:figures/full_fig_p009_12.png] view at source ↗
Figure 14
Figure 14. Figure 14: VyZX constructors and functions visualized using ZXViz. See Section 4 for details on the constructs. parametric proof with an arithmetic solver to prove their soundness. Therefore, our approach allows us a lightweight, Coq rewrite engine compatible, encapsulation of proof irrelevance at the cost of automatically resolvable goals. Lemma stack_assoc : ∀ {n0 n1 n2 m0 m1 m2 : N} (zx0 : ZX n0 m0) (zx1 : ZX n1 … view at source ↗
Figure 15
Figure 15. Figure 15: Select rules from VyZX [PITH_FULL_IMAGE:figures/full_fig_p012_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: A visualization of a selection of VyZX lemmas to express “only connectivity matters” using swaps constructors, we can swap any output of a spider to become the uppermost. We can then remove swaps fully connected to a spider using other lemmas. Bi-algebra rule. Using the expected constructs, we express the bi-algebra rule in VyZX cast free. Note that this rule depends on the associativity of the three-comp… view at source ↗
Figure 17
Figure 17. Figure 17: Construction of sqir operations in VyZX that this model differs from VyZX’s model substantially. While still working based on composed blocks, sqir’s circuits must always have the same number of outputs as inputs. This differs from VyZX, where we can have diagrams with 𝑛 inputs and 𝑚 outputs for any 𝑛 or 𝑚. Moreover, sqir circuit components explicitly specify gate locations instead of stacking diagrams. I… view at source ↗
Figure 18
Figure 18. Figure 18: The peephole optimizations from Figures 4 and 5 in [PITH_FULL_IMAGE:figures/full_fig_p015_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: Example of rewriting structure for reasoning about quantum systems. We also set the foundations for building a verified optimizer based on the ZX-calculus instead of quantum circuits. 7 GRAPHICAL PROOF IN VYZX Every formal verification project must eventually confront proof engineering challenges. In VyZX, it is important to concisely express proofs about the ZX-calculus. To this end, we prove basic facts… view at source ↗
Figure 20
Figure 20. Figure 20: The lemmas we encode in DC⇕AC rendered with ZXViz (rewrite (ZX_compose (ZX_stack zx0 zx1) (ZX_stack zx2 zx3)) (ZX_stack (ZX_compose zx0 zx2) (ZX_compose zx1 zx3)) :when ((= (ZX_m zx0) (ZX_n zx2)) (= (ZX_n zx3) (ZX_m zx1)))) Listing 3. stack_compose_distr translated into egglog where ZX_n and ZX_m are the functions providing dependent type information With the rules in Section 7.1 rules most associativity … view at source ↗
Figure 21
Figure 21. Figure 21: grow_Z_top_left is built by induction using the base lemma grow_Z_left_2_1 [PITH_FULL_IMAGE:figures/full_fig_p019_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Color-swapping the hopf rule, as defined in [PITH_FULL_IMAGE:figures/full_fig_p020_22.png] view at source ↗
Figure 23
Figure 23. Figure 23: ZXViz integrated with the user’s proof writing environment [PITH_FULL_IMAGE:figures/full_fig_p020_23.png] view at source ↗
Figure 24
Figure 24. Figure 24: Proof of Z_absolute_fusion. the gap for ZX-calculus with VyZX. Quantomatic, however, allows for reasoning through adjacency and hence avoid the structural overhead introduced by VyZX, leaving it a useful tool for research on theoretical ZX-calculus results. Similarly, Kissinger [2023] recently released Chyp, an interactive theorem prover for symmetric monoidal categories. It manages a textual and visual r… view at source ↗
Figure 25
Figure 25. Figure 25: Proof of the correctness of bell state preparation in [PITH_FULL_IMAGE:figures/full_fig_p023_25.png] view at source ↗
Figure 26
Figure 26. Figure 26: Directly stateable VyZX rules [PITH_FULL_IMAGE:figures/full_fig_p028_26.png] view at source ↗
Figure 28
Figure 28. Figure 28: The C rule in VyZX [PITH_FULL_IMAGE:figures/full_fig_p030_28.png] view at source ↗
Figure 29
Figure 29. Figure 29: The N rule in VyZX (a) Definition of ⊲ (b) Definition of ⊳ (c) The BW rule [PITH_FULL_IMAGE:figures/full_fig_p031_29.png] view at source ↗
Figure 30
Figure 30. Figure 30: The BW rule in VyZX [PITH_FULL_IMAGE:figures/full_fig_p031_30.png] view at source ↗
read the original abstract

Graphical languages are a convenient shorthand to represent computation, with rewrite rules relating one graph to another. In contrast, proof assistants rely heavily on inductive datatypes, particularly when giving semantics to embedded languages. This creates obstacles to formally reasoning about graphical languages, since imposing an inductive structure obfuscates the diagrammatic nature of graphical languages, along with their corresponding equational theories. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category-theoretic definitions. We developed VyZX to Verify the ZX-calculus, a graphical langauge for reasoning about quantum computation. The ZX-calculus comes with a collection of diagrammatic rewrite rules that preserve the graph's semantic interpretation. We show how inductive graphs in VyZX are used to prove the soundness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. We also provide an IDE-integrated visualizer for proof engineers to directly reason about diagrams in graphical form.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript presents VyZX, a Coq library for formal reasoning about inductively defined graphical languages. It focuses on the ZX-calculus for quantum computation, using category-theoretic inductive graph constructs to prove soundness of the diagrammatic rewrite rules with respect to the standard interpretation, demonstrates practical application via standard proof-assistant techniques, and supplies an IDE-integrated visualizer.

Significance. Machine-checked soundness proofs for ZX rewrite rules would strengthen the foundations for verified quantum computation tools. The work gives explicit credit to the use of inductive datatypes derived from category theory and standard Coq techniques for applying the verified rules.

major comments (2)
  1. [§3] §3 (Inductive definition of ZXGraph): the claim that the inductive datatype 'arises naturally from category-theoretic definitions' and accurately captures the equational theory requires an explicit lemma or theorem establishing that the induced rewrite equivalences match those of the standard ZX-calculus (neither adding spurious equalities nor omitting valid diagrammatic rewrites); no such faithfulness result is stated.
  2. [§5] §5 (Soundness proofs): the soundness theorems are proved inside Coq, but the manuscript supplies no completeness argument or direct comparison of the verified rule set against a reference complete ZX axiomatization (e.g., the known spider-fusion and color-change rules from the literature), leaving open whether the inductive embedding preserves exactly the intended theory.
minor comments (2)
  1. [Abstract] Abstract: the statement that the library was 'used to prove the soundness' would be strengthened by a brief indication of the size or completeness of the verified fragment.
  2. [§4] Notation in §4: the mapping from inductive constructors to standard ZX generators (spiders, wires, etc.) could be presented in a single table for easier cross-reference with the rewrite rules.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments on the manuscript. We respond point-by-point to the major comments below.

read point-by-point responses

  1. Referee: [§3] §3 (Inductive definition of ZXGraph): the claim that the inductive datatype 'arises naturally from category-theoretic definitions' and accurately captures the equational theory requires an explicit lemma or theorem establishing that the induced rewrite equivalences match those of the standard ZX-calculus (neither adding spurious equalities nor omitting valid diagrammatic rewrites); no such faithfulness result is stated.

    Authors: The inductive datatype ZXGraph follows standard category-theoretic constructions for string diagrams and graphical languages. The soundness results establish that the implemented rewrite rules preserve the standard interpretation and thus introduce no spurious equalities. The manuscript does not claim or prove that the datatype and rule set generate exactly the full equational theory of ZX-calculus (i.e., completeness or faithfulness to every valid diagrammatic rewrite). We will revise §3 to state this scope explicitly and remove any phrasing that could be read as asserting full capture of the equational theory without a dedicated lemma. revision: yes

  2. Referee: [§5] §5 (Soundness proofs): the soundness theorems are proved inside Coq, but the manuscript supplies no completeness argument or direct comparison of the verified rule set against a reference complete ZX axiomatization (e.g., the known spider-fusion and color-change rules from the literature), leaving open whether the inductive embedding preserves exactly the intended theory.

    Authors: The contribution of §5 is the machine-checked soundness of the supplied ZX rewrite rules inside the inductive framework. No completeness proof or side-by-side comparison against a reference complete axiomatization is present, because the library is intended as a general tool for verifying soundness of user-chosen rules rather than as a claim that the included rule set is complete. We will add a short discussion in the revised §5 clarifying this distinction and noting that the verified rules form a standard sound subset drawn from the ZX literature. revision: yes

Circularity Check

0 steps flagged

No circularity: soundness proofs target independent external semantics

full rationale

The paper defines inductive graphs from category-theoretic constructions, then uses them to prove soundness of ZX rewrite rules against an external semantic interpretation. No quoted steps reduce a claimed result to a fitted parameter, self-citation chain, or definitional equivalence (e.g., no 'prediction' that is the input by construction). The approach is a standard verification in a proof assistant; the mapping to ZX semantics is presented as an independent check rather than a self-referential derivation. This matches the default expectation of a non-circular verification paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on the domain assumption that category-theoretic definitions naturally yield inductive graph structures whose equational theory matches the graphical language; no free parameters or invented entities are mentioned.

axioms (1)
  • domain assumption Category-theoretic definitions provide inductive structures for graphical languages that preserve their equational theories.
    Explicitly stated in the abstract as the origin of the inductive constructs used in VyZX.

pith-pipeline@v0.9.0 · 5703 in / 1155 out tokens · 26110 ms · 2026-05-24T06:18:00.268139+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 2 Pith papers

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

  1. TensorRocq: Enabling diagrammatic reasoning in Rocq

    cs.LO 2026-04 unverdicted novelty 7.0

    TensorRocq supplies verified Rocq tactics that convert symmetric monoidal category terms to hypergraphs with interfaces, enabling equivalence inference and rewriting based on string-diagram deformations while preservi...

  2. Typed compositional quantum computation with lenses

    cs.PL 2023-11 unverdicted novelty 7.0

    Coq framework with discrete lenses for typed, compositional definition and verification of quantum circuits.

Reference graph

Works this paper leans on

2 extracted references · 2 canonical work pages · cited by 2 Pith papers

  1. [1]

    Ambroise Lafont

    Springer, 326–336. Ambroise Lafont. 2023. A Diagram Editor to Mechanize Categorical Proofs. https://amblafont.github.io/articles/yade.pdf. Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, and Michael Hicks. 2022. Verified Compilation of Quantum Oracles. Proceedings of the ACM on Programming Languages 6, OOPSLA2, Article 146 (October 2022), ...

    work page doi:10.1145/3563309 2023

  2. [2]

    CoqQ : Foundational verification of quantum programs

    Better Together: Unifying Datalog and Equality Saturation. arXiv:2304.04332 [cs.PL] Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. 2023. CoqQ: Foundational Verification of Quantum Programs. Proceedings of the ACM on Programming Languages 7, POPL, Article 29 (January 2023), 29 pages. https://doi.org/10.1145/3571222 arXiv:2207.113...

    work page doi:10.1145/3571222 2023