PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Arun Govindankutty

arXiv:2610.03794v1quant-phcs.ETcs.LO

TL;DR

Quantum-circuit verification is difficult at scale because the state space grows exponentially. This paper extends a bit-vector abstraction for H, X, and C-NOT circuits, proves soundness within a characterized fragment, and evaluates code verification, fault detection, and scalability. Its experiments support verification across the studied circuit classes, while identifying limits tied to constraint structures, decoder properties, and the abstraction's scope.

  • Problem

    Quantum-circuit verification faces exponentially growing state spaces, and the earlier abstraction's generality, soundness conditions, systematic fault-detection effectiveness, and scalability sources remained unresolved.

    Source: §1 · p. 2, §4.6 · p. 16

  • Method

    The paper extends a bit-vector abstraction that tracks abstract basis bits and Hadamard tags, and characterizes a circuit fragment where it faithfully represents Hilbert-space semantics.

    Source: §4.1 · p. 10, §4.6 · pp. 16–17

  • Results

    The experiments verify the studied parametrised and CSS-code properties, distinguish error-handling limits, and report scalable GHZ verification alongside higher costs for some constraint structures and decoder properties.

    Source: §6.11 · p. 40

  • Takeaways & Limitations

    The results support using the abstraction for the circuit classes studied, while revealing constraint structures and decoder properties associated with higher verification costs.

    Source: §6.11 · p. 40

    Circuits outside fragment F—including Hadamards on entangled qubits, S or Z gates, and superposition data qubits acting as C-NOT controls between Hadamards—require a richer abstract state and remain future work.

    Source: §7.6 · p. 43

Abstract

from arXiv · show

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.

1 Introduction

Formal quantum-circuit verification must address exponentially growing state spaces, while earlier work left open whether its bit-vector abstraction generalises to broader code families and has a soundness characterisation. This article extends that framework to parametrised and CSS codes, proves its soundness within a defined circuit fragment, and evaluates fault detection and scalability.

1 Introduction

  • Formal verification faces exponentially growing state spaces, while earlier abstraction results left generalisation, CSS applicability, soundness, systematic fault validation, and scalability explanations unresolved.Earlier studies cited in the introduction reported verification up to 96 qubits, 10 qubits, and 128 qubits using other approaches.Source: §1 · p. 2
  • Repetition-code properties extend to arbitrary n-qubit bit-flip codes and k-block concatenated phase-flip codes, with n and k verified up to 101.The bit-flip construction uses n −1 syndrome ancillas.Source: §1 · p. 2
  • Within the restricted {H, X, C-NOT} gate set, bit-flip and phase-flip syndrome extraction is formally verified for the Steane, [[15, 7, 3]] quantum Hamming, [[15, 1, 3]] quantum Reed-Muller, and rotated surface codes up to distance 101.Source: §1 · p. 3
  • The framework checks arbitrary error patterns, detection up to a specified weight, and decoder-based recovery, with negative cases yielding undetectable or incorrectly corrected patterns.The recovery process applies a classically controlled correction after decoding.Source: §1 · p. 3
  • The authors prove soundness for a defined {H, X, C-NOT} fragment, show each defining condition is necessary, test against state-vector simulation, and prove Lemmas 1–6 from [1].The lemmas are presented as exact characterisations of modifications detected by the abstraction.Source: §1 · p. 3
  • Mutation testing identifies equivalent mutants and detects all 622 non-equivalent mutants within a fault model spanning 13 operators and 12 circuit families.Equivalent mutants are excluded from evaluation using an SMT miter.Source: §1 · p. 3
  • A Z3 Python API implementation verifies GHZ circuits with up to 262,144 qubits on a 16 GB laptop across three topologies, while random-network costs rise with depth.A controlled ablation indicates that neither the encoding pipeline nor solver version explains the improvement over [1].Source: §1 · p. 3

2 Theoretical Background

This background introduces quantum states and entanglement, error-correcting codes, CSS parity checks, and the terminology used for error handling. It also motivates formal verification as a way to reason over circuit behaviours despite the exponential state space.

2 Theoretical Background

  • An n-qubit system has a state vector in a 2^n-dimensional Hilbert space, making direct circuit analysis computationally expensive as system size grows.Quantum circuits are ordered sequences of gates that transform input states into desired outputs.Source: §2 · pp. 4–5

2.1 Entanglement: Bell and GHZ states

  • Bell and GHZ states illustrate entanglement, which means a multi-qubit state cannot be expressed as a tensor product of its individual qubit states.A GHZ state uses one Hadamard gate followed by m −1 C-NOT gates.Source: §2.1 · p. 5

2.2 Quantum errors and repetition codes

  • Repetition codes encode logical information across physical qubits and detect bit flips by accumulating parity checks on ancillas without directly measuring the encoded state.The Shor nine-qubit code combines bit-flip and phase-flip protection using transformed repetition-code blocks.Source: §2.2 · pp. 5–6

2.3 Classical linear codes and the CSS construction

  • CSS codes use two parity-check matrices for X- and Z-type stabilizers, with syndrome extraction reducing bit-flip and phase-flip detection to classical parity checks.The Steane code uses the Hamming(7, 4) parity-check matrix for both matrices; the considered codes also include Hamming, Reed-Muller, and rotated surface codes.Source: §2.3 · pp. 6–7

2.4 Error detection, identification, decoding, recovery, and fault tolerance

  • Here, detection requires a non-zero syndrome, identification requires a unique syndrome up to stabilizers, decoding maps a syndrome to a correction, and recovery applies it.Fault tolerance is outside the abstraction's scope and requires extraction and recovery circuits to tolerate faults without spreading them into uncorrectable data errors.Source: §2.4 · p. 7

2.5 Formal verification

  • Formal verification checks specifications over all possible behaviours, and this work builds on an SMT bit-vector abstraction for H, X, and C-NOT circuits.The framework extends that approach to generalised circuit families and CSS codes, with formal verification and mutation-based validation.Source: §2.5 · p. 7

3 Related Work

Prior quantum-circuit verification work uses several representations with differing trade-offs between expressiveness and scalability. This article extends a bit-vector abstraction and distinguishes its universally quantified verification from stabilizer simulation.

3 Related Work

  • Rewrite-rule verification was reported for circuits up to 96 qubits, with larger instances limited by integer-overflow issues.The cited method uses dyadic arithmetic and rewrite rules in a Haskell theorem prover.Source: §3 · p. 8
  • Decision-diagram verification was reported for circuits up to 10 qubits, and its effectiveness decreases as entanglement increases.The cited work applied multiple-valued decision diagrams to properties including Grover implementations.Source: §3 · p. 8
  • Equivalence-checking methods compare an implementation with a trusted reference and use Hilbert-space representations when binary-space reductions do not apply.The cited evaluations included circuits up to 128 qubits.Source: §3 · p. 8
  • Earlier bit-vector abstractions verified Bell, GHZ, and fixed-size error-detection circuits, but considered only fixed code sizes and left correctness lemmas unproved.The present work extends the framework to arbitrary repetition-code families, CSS codes, soundness proofs, and mutation-based fault injection.Source: §3 · pp. 8–9
  • Stabilizer simulation applies in polynomial time to the full Clifford group, whereas this abstraction is limited to fragment F and checks properties over all admissible inputs and error patterns.The paper cautions that its scalability results do not show greater efficiency than stabilizer simulation.Source: §3 · p. 8
  • Mutation testing addresses equivalent mutants, which may be functionally identical to the original; for these finite-state abstract circuits, equivalence is decidable and checked using an SMT miter.The article applies mutation-based fault injection to evaluate verification properties.Source: §3 · p. 9

4 Verification Framework

The verification framework extends the bit-vector abstraction to parametrised code families, CSS syndrome extraction, multiple-error detection, and recovery, while formalising when it soundly represents concrete circuits. It also examines which circuit modifications correctness checks detect, including equivalent mutations that can cancel.

4.1 Base abstraction

  • Each abstract qubit uses a 3-bit superposition tag and a 2-bit measurement/basis vector; the framework distinguishes branch and frame readings for the basis bit.Hadamard updates the tag with saturation so its parity is preserved and zero remains the no-Hadamard value; the two readings support Bell/GHZ circuits and phase-flip detection, respectively.Source: §4.1 · pp. 9–10

4.2 Base correctness properties

  • The earlier framework [1] defines correctness properties for bit-flip detection, phase-flip detection, and entanglement-generation circuits.These properties specify expected ancilla initialization and measurement, superposition behavior, parity syndromes, and entanglement outputs.Source: §4.2 · pp. 11–12

4.3 Generalised properties for parametrised code families

  • Generalised repetition and concatenated-code properties extend verification to parametrised families, with adjacent-block parity syndromes identifying a single erroneous bit or block.For concatenated codes, the syndrome is all zero without an error and uniquely identifies the erroneous block when exactly one block is affected.Source: §4.3 · pp. 12–13

4.4 The Steane [[7, 1, 3]] CSS code

  • The Steane construction maps a single error at qubit k to the binary representation of k + 1, and general CSS extraction measures syndromes He using HZ or HX.The arbitrary CSS construction uses HZ for bit-flip errors and HX for phase-flip errors; the measured ancilla vector equals He for at most one error.Source: §4.4 · p. 14

4.5 Multiple errors, detection, and recovery

  • For arbitrary error patterns, syndrome correctness requires the measured ancillas to equal He modulo 2 and the data values to remain unchanged by extraction.The section also specifies detection up to weight w by requiring a non-zero syndrome, and defines recovery through an operation depending only on the measured syndrome.Source: §4.5 · p. 15
  • For a code of distance d, detection is expected through weight d −1 but to fail at d, while recovery is expected through ⌊(d −1)/2⌋ and to fail at the next weight.Recovery uses a minimum-weight decoder for repetition codes and a lookup decoder for CSS codes with distinct non-zero check-matrix columns; negative cases yield undetectable or incorrectly corrected errors.Source: §4.5 · p. 15

4.6 Soundness of the abstraction

  • For circuits in fragment F, the abstraction is sound, and an unsatisfiable query for a property transfers its basis-value and tag conditions to concrete outputs.F requires computational qubits to receive no Hadamards, branch qubits to receive exactly one before any C-NOT, and frame qubits to receive paired Hadamards with no intervening gates except injected phase-flip errors. Measurements and classically controlled X gates apply only to even-tag qubits after their gates are complete; syndrome outcomes fixed by error variables are deterministic and do not disturb admissible logical superpositions.Source: §4.6 · pp. 16, 18
  • The abstraction is incomplete and unsound outside F; counterexamples show violations when gates occur inside frame segments or Hadamards follow entangling C-NOT gates.It omits relative phases and counts Hadamards in tags, so functionally redundant Hadamard pairs can cause conservative false alarms; representing phase-sensitive gates such as S would require explicit phase information.Source: §4.6 · p. 18

4.7 Proofs of Lemmas 1-6

  • Lemmas 1–4 characterize detection of ancilla initialization, Hadamard, and syndrome-extraction modifications, with C-NOT changes detected exactly when they alter an ancilla parity set.The lemmas also establish that functionally equivalent changes, such as reordering C-NOT gates on the same ancilla, are not detected by functional properties.Source: §4.7 · pp. 19–20
  • Lemma 5 detects Bell- or GHZ-circuit changes exactly when they alter a qubit’s Hadamard count or output basis-bit function, and Lemma 6 extends this criterion to combinations of modifications.Rewiring a GHZ C-NOT to a control already carrying the GHZ value leaves the computed functions unchanged and is correctly not reported.Source: §4.7 · pp. 20–21
  • Two identical extra CNOT gates on the same ancilla can cancel, leaving parity unchanged and making the circuit functionally equivalent to the intended circuit.The SMT solver checks each property over all admissible assignments, so one counterexample rejects a circuit; mutation experiments in Section 6.10 empirically confirm this characterization.Source: §4.7 · p. 21

5 Verification Methodology

The methodology encodes circuit behavior and correctness properties as SMT constraints, then uses mutation testing and controlled experiments to evaluate the framework and its implementation.

5.1 SMT encoding and verification

  • Verification asserts the circuit constraints and the negated property: unsat establishes correctness for valid symbolic inputs, while sat yields a counterexample.For circuits in F, Corollary 1 transfers an unsat result to the corresponding concrete circuit.Source: §5.1 · p. 21
  • The encoding has O(n + gH + gX + gC) gate-level size, but solving time depends on constraint structure, dense XOR dependencies, cardinality constraints, and decoder-based recovery queries.For CSS circuits, encoding size is O(N + nnz(H)); linear encoding size does not imply linear solving time.Source: §5.1 · p. 22

5.2 Mutation-based fault injection

  • Mutation testing applies fault operators at valid locations, mechanically excludes equivalent mutants with a complete SMT-miter test, and checks remaining mutants against the correctness property.The mutation study validates the implementation against Lemmas 1–6; it is not an independent soundness validation.Source: §5.2 · pp. 22–23
  • The mutation sweep covers every valid operator location, avoiding manual selection and making the full sweep reproducible.Mutants with nonexistent target locations are reported as not generated.Source: §5.2 · p. 22

5.3 Experimental setup

  • Experiments use Z3 on a 16 GB MacBook, with repeated fresh-solver runs and separately reported build and solve times.Random-network configurations use three seeds; solve-time repetitions vary for the largest GHZ, surface-code, and multi-error instances.Source: §5.3 · pp. 23–24

6 Experimental Results

The experiments reproduce the earlier fixed-size benchmarks and test correctness and runtime as repetition and concatenated phase-flip codes grow. All tested instances satisfy their properties, with solve time increasing approximately linearly for the generalized families.

6.1 Baseline reproduction

  • All reproduced fixed-size benchmark circuits verify in about one millisecond, with standard deviations of a few percent of the median.The results reproduce the earlier study [1] using different hardware and direct Z3 API encoding.Source: §6.1 · p. 24, Table 4 · p. 24

6.2 Generalised repetition and concatenated phase-flip codes

  • 32.8 ms and 38.0 ms: the largest generalized repetition and concatenated phase-flip instances, respectively, verify successfully, with solve time increasing approximately linearly with code size.Both families were tested up to 101 logical elements; the concatenated-code model uses one abstract block-qubit per three-qubit block.Source: §6.2 · p. 25, Table 5 · p. 25, Figure 1 · p. 26

6.3 CSS syndrome extraction

The framework verifies syndrome extraction across CSS codes with varied parity-check structures, then tests detection and recovery boundaries across error weights. Its results match expected code capabilities, while minimum-weight repetition-code recovery becomes expensive at larger sizes.

6.3 CSS syndrome extraction

  • The evaluation covers four CSS families, including codes with unequal check matrices and local surface-code checks, using matrices generated and checked before verification.It checks the CSS condition, logical-qubit counts, and distances by exhaustive enumeration for codes with N ≤ 25.Source: §6.3 · p. 26
  • All tested syndrome-extraction circuits pass, including rotated surface codes through distance 101 (15,301 data and ancilla qubits) in 160s.For surface codes, solve time rises from 0.278s at d = 21 to 160s at d = 101.Source: §6.3 · p. 26, Table 7 · p. 27, Table 6 · p. 27

6.4 Multiple errors, detection, and recovery

  • All 60 multi-error outcomes agree with coding theory: detection holds through weight d−1, while weight d yields an undetectable pattern.For the Steane code, the weight-3 counterexample is a logical operator.Source: §6.4 · p. 29, Table 8 · p. 30
  • Recovery holds through weight ⌊(d −1)/2⌋, with miscorrection at the next weight; Reed-Muller detection is asymmetric at weights 6 for bit flips and 2 for phase flips.For Steane, two bit flips can produce the syndrome associated with a third qubit.Source: §6.4 · p. 29
  • Minimum-weight repetition-code recovery is costly: n = 21 takes 69.2s, and a preliminary n = 31 run exceeds 120s.Look-up and syndrome-only properties remain inexpensive.Source: §6.4 · p. 29

6.5 Scalability for GHZ-state verification

The evaluation verifies GHZ circuits across three topologies up to 262,144 qubits. Solve time scales approximately linearly with circuit size, while construction time and memory become the larger costs at the largest instances.

6.5 Scalability for GHZ-state verification

  • At 262,144 qubits, all three GHZ topologies verify: solve times are 9.01s for star, 13.0s for chain, and 12.3s for tree.The reported comparison is summarized for three topologies in Table 9 and Figure 3.Source: §6.5 · p. 31, Table 9 · p. 31, Figure 3 · p. 32
  • Solve time grows approximately linearly across the evaluated sizes, with topology changing it by less than 50%; chain is slowest and star fastest.The circuits use star, nearest-neighbour chain, and logarithmic-depth tree topologies.Source: §6.5 · p. 31, Figure 3 · p. 32
  • For the largest star instance, Python-side construction takes 46.1s versus 9.01s to solve, and peak memory reaches 1,397MiB.Memory use is about 5.3KiB per qubit, with construction also dominating peak memory.Source: §6.5 · p. 31, Table 9 · p. 31, Figure 3 · p. 32

6.6 Encoding size

GHZ encoding size grows linearly with qubit count, but verification of random H+C-NOT networks becomes sharply harder as depth and output support increase. This contrast limits the favorable scaling observed for sparse circuit structures.

6.6 Encoding size

  • SMT variables, assertions, and bit-blasted CNF clauses all grow linearly with qubit count; GHZ encodings use about 6.5 clauses per qubit for star and 7.0 for chain and tree.Table 10 reports query sizes for representative code and surface-code instances as well as GHZ circuits.Source: §6.6 · p. 32, Table 10 · p. 33

6.7 Random H+C-NOT networks

  • Random networks apply Hadamards to a random half of the qubits before depth-D layers of randomly oriented C-NOT pairs and sparse X gates; output support grows rapidly with depth.The tested property compares output basis bits with independently derived GF(2) affine functions and checks the Hadamard-qubit tags.Source: §6.7 · p. 33
  • For 32 qubits, median solve time rises from 0.033s at depth 4 to 27s at depth 7, with two of three depth-8 seeds exceeding 300s.At 64 qubits, median time rises from 0.20s at depth 5 to 125s at depth 7; the reported circuits remain small.Source: §6.7 · p. 33, Table 11 · p. 34, Figure 4 · p. 35

6.8 Controlled ablation of encoding pipeline and solver version

Controlled ablations compare API and SMT-LIB pipelines on identical GHZ-star constraints and compare two Z3 releases on the same machine. Neither pipeline nor solver version explains the observed difference from prior work, which remains observational.

6.8 Controlled ablation of encoding pipeline and solver version

  • For identical constraints, the stand-alone Z3 executable solves the 262,144-qubit SMT-LIB query in 5.0s, versus 8.8s for the API-built query.The SMT-LIB pipeline is not slower overall; serialization and parsing add 4.1s and 1.9s for the 50MB file.Source: §6.8 · p. 36, Table 12 · p. 36
  • The direct API's practical advantage is avoiding intermediate files and supporting programmatic construction of circuit families, mutants, and miters, not faster solving.The measured time difference appears related to term structure, which the authors did not investigate further.Source: §6.8 · p. 36
  • Z3 4.13.4 and 5.1.0 are within about 25% at tested sizes and give identical solve times at the largest size.Table 13 reports median solve time with standard deviation.Source: §6.8 · p. 36, Table 13 · p. 36
  • The source of the difference from [1] remains unresolved because the ablations do not reproduce its generator, constraint form, or hardware.The comparison with [1] is treated as observational only.Source: §6.8 · pp. 36–37

6.9 Differential validation of the soundness theorem

Differential testing agrees with the abstraction on its soundness fragment and exposes disagreements outside it. Mutation testing detects every non-equivalent mutant in the evaluated fault model.

6.9 Differential validation of the soundness theorem

  • All 12,000 circuits in F agreed with state-vector simulation for every input, while unrestricted random circuits agreed only about 55% of the time.The test included 1,528 circuits with saturated tags; counterexamples C1-C4 each produced a disagreement.Source: Table 14 · p. 37, §6.9 · p. 37

6.10 Mutation-based validation

  • The SMT miter classified 60 generated mutants as equivalent; all were reordered commuting C-NOT gates, and they were excluded from fault-detection analysis.The evaluation generated 682 mutants across 12 circuit families; 12 additional mutations had no valid location.Source: §6.10 · p. 37
  • The 100% detection result applies only to the evaluated mutation classes and circuit instances, not to complete fault coverage.It provides empirical evidence for the implementation fault classes considered in the study.Source: §6.10 · p. 37
  • Every one of the 622 non-equivalent mutants violated its corresponding property, yielding 100% detection across circuit families and mutation operators.Tables 15 and 16 and Figure 5 report the mutation results.Source: §6.10 · p. 37, Table 15 · p. 38, Table 16 · p. 38

6.11 Discussion of results

The experiments cover parametrised code families, CSS syndrome extraction, multiple-error properties, and large GHZ circuits. Together, they show that verification scales for the studied circuit classes while exposing structures that increase cost.

6.11 Discussion of results

  • The abstraction verifies the benchmark circuits considered, with parametrised repetition and concatenated phase-flip families and syndrome extraction for arbitrary CSS check matrices.Multiple-error experiments distinguish detection, identification, and recovery, and confirm the expected limits of the codes studied.Source: §6.11 · p. 40
  • GHZ verification scales beyond 2.6×10^5 qubits across all three evaluated topologies, while random-network and recovery experiments reveal limits to that scaling.The experiments provide an independent check of the soundness theorem on its stated fragment and show failure outside it.Source: §6.11 · p. 40
  • The studied framework handles substantial scale while identifying constraint structures and decoder properties associated with higher verification costs.The results concern the circuit classes investigated.Source: §6.11 · p. 40

7 Discussion: Scope, Limitations, and Threats to Validity

The discussion bounds the abstraction to a proper subset of H, X, and C-NOT circuits and distinguishes circuit-level verification from physical validation.

7.1 Scope of the abstraction

  • The abstraction is sound for fragment F, a proper subset of H, X, and C-NOT circuits, and is not a method for general stabilizer circuits.F covers the circuit families studied, but physical bit-flip faults inside a Hadamard frame segment fall outside its model.Source: §7.1 · p. 40
  • Codes with intrinsic Y-type stabilizers, including the five-qubit perfect code, require additional phase-aware semantics beyond the current abstraction.The proposed extension would add an abstract S gate and representation of relative phases.Source: §7.1 · p. 40
  • Circuit-level verification does not model hardware noise or establish that a physical device implements the verified circuit correctly.Device validation and realistic logical error-rate estimation require complementary methods.Source: §7.1 · p. 41

7.2 Detection, correction, and fault tolerance

  • The verified error variables act before syndrome extraction, whose circuit is assumed fault-free; faults during extraction and their propagation are not modeled.Ancilla faults can propagate as hook errors, and the Steane result verifies classical Hamming(7, 4) syndrome logic in both Pauli frames, not fault tolerance of the full extraction circuit.Source: §7.2 · p. 41

7.3 Error model and preconditions

  • Single-error properties assume at most one error and, for Steane and CSS checks, a valid input code word; extraction, recovery, measurement, and repeated-round errors are outside the current model.Properties 8-10 separately cover arbitrary error patterns and specified detection or recovery weights.Source: §7.3 · pp. 41–42

7.4 Coverage of the mutation analysis

  • The mutation study tests single injected modifications from listed operator classes and instances, so its 100% detection rate is not complete or physically realistic fault coverage.Systematic combinations of simultaneous faults and other fault classes were not evaluated.Source: §7.4 · p. 42

7.5 Interpretation of the scalability results

  • Reported GHZ scale reflects sparse XOR relationships, not arbitrary circuits; random networks with outputs depending on many inputs become harder as depth increases.The comparison with [1] is observational rather than controlled, and the SMT task checks properties across admissible inputs and error patterns rather than simulating GHZ circuits.Source: §7.5 · pp. 42–43
  • Beyond 262,144 qubits, Python-side construction and memory—not solver time—are the main resource limits; the 16 GB test machine suggests a limit near three million qubits.At the largest tested size, construction took 46s versus 9s for solving, and memory grew about 5.3 KiB per qubit.Source: §7.5 · p. 43

8 Conclusion and Future Directions

The paper extends the bit-vector abstraction to broader circuit families and establishes theoretical and empirical support within its scope. It identifies phase-aware and fault-tolerant extensions as future directions.

8 Conclusion and Future Directions

  • The paper extends the abstraction to parametrised repetition and concatenated codes, Steane CSS verification, a soundness theorem, complete proofs of six lemmas, mutation testing, and direct Z3 encoding.The conclusion reports that 120 mutants were detected and that the reimplementation enabled GHZ verification at substantially larger scales with fewer computational resources than previously reported.Source: §8 · p. 44
  • The results indicate that the abstraction reaches beyond the fixed-size examples of the original study while maintaining efficient SMT-based verification across a broader class of circuits.The conclusion emphasizes generalised properties, Steane-code verification, and theoretical and empirical analyses.Source: §8 · p. 44
  • Future work includes representing relative phase to support genuine Y-type operators, modelling simultaneous errors and recovery for fault-tolerant protocols, and extending mutation-based validation..Source: §8 · p. 44
Loading 2610.03794v1…