Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over $$\{H,X,{\text{C-NOT}}\}$$: CSS Constructions, Soundness, and Mutation-Based Validation

Abstract Formal verification of quantum circuits becomes increasingly difficult as circuit size increases, since exhaustive reasoning over the underlying Hilbert space is computationally expensive. In previous work [1], we introduced a bit-vector abstraction that separates the tracking of superposition from basis-state behaviour, enabling SMT-based verification of fixed-size error-detection and entanglement circuits constructed from H , X , and C-NOT gates. This paper extends that framework in five directions. First, we generalise the 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 code, the [[15, 7, 3]] quantum Hamming code, the [[15, 1, 3]] quantum Reed–Muller code, and rotated surface codes with distances up to 101. The verification considers arbitrary error patterns, error detection up to a specified weight, and recovery using a classical decoder. Counterexamples are obtained for errors beyond the correction or detection capability of the respective codes. Third, we characterise the fragment of $$\{H,X,\text {C-NOT}\}$$ circuits for which the abstraction faithfully represents the corresponding Hilbert-space semantics. We prove soundness for this fragment, demonstrate the necessity of the stated conditions through counterexamples, validate the characterisation by differential testing against state-vector simulation, and prove the six lemmas established in the original work. Fourth, we conduct a mutation study using 13 mutation operators and automatically identify equivalent mutants. Within the evaluated fault model, the approach detects all 622 non-equivalent mutants. Fifth, we implement the approach directly using the Z3 API and verify GHZ circuits with up to 262,144 qubits across three topologies on a 16 GB laptop. The evaluation includes repeated measurements and a controlled ablation of the encoding pipeline and solver version. Experiments with random H +C-NOT networks show that verification cost increases steeply with circuit depth when outputs depend on a large number of inputs. The approach is not intended to cover general stabiliser circuits, Y -type stabilisers, fault-tolerant protocols, or physical noise. We identify the extensions required to address these cases.