{
  "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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": "2610.03794",
  "author_total": 1,
  "authors": [
    {
      "name": "Arun Govindankutty"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/83q0cxj7ebs6t.bib",
  "cited_by": 0,
  "doi": "10.48550/arxiv.2610.03794",
  "fulltext_url": null,
  "id": "83q0cxj7ebs6t",
  "issns": [],
  "landing_url": "https://arxiv.org/abs/2610.03794",
  "language": null,
  "licence": "LicenseRef-arXiv-nonexclusive-1.0",
  "licence_label": "arXiv licence",
  "licence_source": "article",
  "licence_url": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
  "metadata_licence": "CC0-1.0",
  "native_subjects": [
    [
      "arxiv",
      "cs.ET"
    ],
    [
      "arxiv",
      "cs.LO"
    ],
    [
      "arxiv",
      "quant-ph"
    ]
  ],
  "openalex": null,
  "pdf_url": "https://arxiv.org/pdf/2610.03794",
  "pmcid": null,
  "pmid": null,
  "published": "2026-10-01",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/83q0cxj7ebs6t.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:29:50Z",
      "native_id": "2610.03794",
      "source": "arxiv",
      "url": "https://arxiv.org/abs/2610.03794"
    }
  ],
  "subjects": [
    {
      "field": "physics",
      "origin": "arxiv:quant-ph",
      "subfield": "quantum"
    }
  ],
  "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",
  "title_text": "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",
  "type": "preprint",
  "updated_at": "2026-10-30T12:29:50Z",
  "url": "https://research.draconitic.com/paper/83q0cxj7ebs6t",
  "venue": "arXiv",
  "versions": [
    {
      "doi": "10.1007/s42979-026-05395-6",
      "pid": null,
      "relation": "published-as",
      "title": null,
      "venue": null
    }
  ]
}