VyZX: Formal Verification of a Graphical Quantum Language
Adrian Lehmann, Ben Caldwell, Bhakti Shah, Robert Rand
TL;DR
VyZX addresses the challenge of formally verifying graphical languages by encoding ZX-diagrams as inductive graphs with a denotational semantics in complex matrices, enabling sound diagrammatic proofs that align with matrix ground truth. The framework combines Coq-based inductive ZX-diagrams, a parametric and compositional representation, a visualizer (ZXViz), and automation for color-swaps, transposes, casts, and induction, along with a complete ZX-calculus rule set implemented graphically. It demonstrates circuit ingestion from SQIR, peephole optimizations, and fully diagrammatic proofs for core ZX rules, providing interoperability with QuantumLib-based tools and establishing a practical workflow for verified quantum graphics. The work shows how inductive structure and visualization can reduce proof overhead, improve readability, and enable extraction and verification of software manipulating ZX-diagrams, paving the way for verified quantum optimizers and broader categorical diagrammatic reasoning. Overall, VyZX offers a robust, extensible platform for diagrammatic verification in quantum computing and beyond, combining formal semantics, automated reasoning, and user-friendly visualization.
Abstract
Mathematical representations of graphs often resemble adjacency matrices or lists, representations that facilitate whiteboard reasoning and algorithm design. In the realm of proof assistants, inductive representations effectively define semantics for formal reasoning. This highlights a gap where algorithm design and proof assistants require a fundamentally different structure of graphs, particularly for process theories which represent programs using graphs. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category theory definitions. A key goal for VyZX is to Verify the ZX-calculus, a graphical language 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 correctness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. VyZX integrates easily with the proof engineer's workflow through visualization and automation.