VyZX: Formal Verification of a Graphical Quantum Language

TL;DR

VyZX is a verified library that enables formal reasoning about graphical quantum languages like ZX-calculus, bridging the gap between diagrammatic reasoning and proof assistants.

Contribution

It introduces VyZX, a novel inductive framework for verifying graphical languages, specifically applied to the ZX-calculus for quantum computation.

Findings

VyZX proves the soundness of ZX-calculus rewrite rules.

The library supports practical reasoning with diagrams using proof assistant techniques.

An IDE-integrated visualizer enhances diagrammatic reasoning.

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.