Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over {H,X,C-NOT}: CSS Constructions, Soundness, and Mutation-Based Validation
Abstract
Formal verification of quantum circuits becomes difficult as circuit size grows because exhaustive reasoning over the Hilbert space is computationally expensive. In previous work [1], we introduced a bit-vector abstraction that separates superposition tracking from basis-state behavior, enabling SMT-based verification of fixed-size error-detection and entanglement circuits built from H, X, and C-NOT gates. This paper extends the framework in five directions. First, we generalise correctness properties to parametrised repetition and concatenated phase-flip codes with up to 101 logical elements. Second, we verify syndrome extraction for CSS codes specified by arbitrary parity-check matrices, including the Steane, [[15,7,3]] Hamming, [[15,1,3]] Reed-Muller, and rotated surface codes with distances up to 101. We consider arbitrary error patterns, detection up to a specified weight, and recovery using a classical decoder, with counterexamples beyond each code's correction or detection capability. Third, we characterize the {H,X,C-NOT} fragment for which the abstraction faithfully represents Hilbert-space semantics. We prove soundness, demonstrate necessity with counterexamples, validate the characterisation against state-vector simulation, and prove the six lemmas from the original work. Fourth, a mutation study using 13 operators identifies equivalent mutants and detects all 622 non-equivalent mutants within the evaluated fault model. Fifth, a direct Z3 implementation verifies GHZ circuits with up to 262,144 qubits across three topologies on a 16GB laptop. Random H+C-NOT networks show verification cost rises sharply with depth when outputs depend on many inputs. The approach does not target general stabilizer circuits, Y-type stabilizers, fault-tolerant protocols, or physical noise; we identify extensions needed to address these cases.
Versions
Related
- Generalised entanglement wedges in three dimensions
- Simple proof of conditions requiring maximal entanglement for local state verification and discrimination
- Breaking the Bounded Entanglement Barrier for Quantum Position Verification
- Outram Park Part II: Agentic Verification, Validation and Documentation as a Human Review Gate for Nuclear Data and Neutronics Software
- Agentic Porting, Construction and Initial Verification and Validation of Libraries within the Open Source Unified TRAnsient Multi-Phase Advanced Reactor simulation Kit (Outram Park) Part I: A Software Engineering Log for Thermal Hydraulics
BibTeX
@misc{govindankutty2026generalised,
title = {{Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over H,X,C-NOT: CSS Constructions, Soundness, and Mutation-Based Validation}},
author = {Arun Govindankutty},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.03794},
eprint = {2610.03794},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.03794},
}
RIS
TY - UNPB
TI - Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over {H,X,C-NOT}: CSS Constructions, Soundness, and Mutation-Based Validation
AU - Arun Govindankutty
PY - 2026
DA - 2026/10/01
PB - arXiv
DO - 10.48550/arxiv.2610.03794
UR - https://arxiv.org/abs/2610.03794
AB - Formal verification of quantum circuits becomes difficult as circuit size grows because exhaustive reasoning over the Hilbert space is computationally expensive. In previous work [1], we introduced a bit-vector abstraction that separates superposition tracking from basis-state behavior, enabling SMT-based verification of fixed-size error-detection and entanglement circuits built from H, X, and C-NOT gates. This paper extends the framework in five directions. First, we generalise correctness properties to parametrised repetition and concatenated phase-flip codes with up to 101 logical elements. Second, we verify syndrome extraction for CSS codes specified by arbitrary parity-check matrices, including the Steane, [[15,7,3]] Hamming, [[15,1,3]] Reed-Muller, and rotated surface codes with distances up to 101. We consider arbitrary error patterns, detection up to a specified weight, and recovery using a classical decoder, with counterexamples beyond each code's correction or detection capability. Third, we characterize the {H,X,C-NOT} fragment for which the abstraction faithfully represents Hilbert-space semantics. We prove soundness, demonstrate necessity with counterexamples, validate the characterisation against state-vector simulation, and prove the six lemmas from the original work. Fourth, a mutation study using 13 operators identifies equivalent mutants and detects all 622 non-equivalent mutants within the evaluated fault model. Fifth, a direct Z3 implementation verifies GHZ circuits with up to 262,144 qubits across three topologies on a 16GB laptop. Random H+C-NOT networks show verification cost rises sharply with depth when outputs depend on many inputs. The approach does not target general stabilizer circuits, Y-type stabilizers, fault-tolerant protocols, or physical noise; we identify extensions needed to address these cases.
ER -