A quantum error correction decoder is a library other people's results depend on, judged in one dominant way. Sample errors, decode, and count wrong logical observables. We ask what else can be checked there. Our conformance contract needs no oracle. One check asks that a returned correction explain the syndrome in the caller's index space. The other hands a decoder one instance under two presentations differing only in bookkeeping, where two feasible corrections of different weight prove the heavier is not minimum-weight. Verdicts are gated on what each library declares, so a firing contradicts a published guarantee. Nine configurations from five public libraries give three results. Documentation answers 4 of 54 capability questions. Bounded-distance correctness, the property callers most depend on, has a direct declaration yield of 0.0%, though its hypotheses hold in 62.1% of cases. Presentation sensitivity is real but shallow. One solver moved to a 26% heavier correction under a different numbering, which reaches the logical class at most once in twenty thousand shots. Established evaluation misses corruptions that preserve logical parity, while one summation over the caller's weights catches every one we injected. All 639 certificates ship as bundles a standalone verifier re-derives from first principles.
A quantum error correction decoder is a library other people's results depend on, judged in one dominant way. Sample errors, decode, and count wrong logical observables. We ask what else can be checked there. Our conformance contract needs no oracle. One check asks that a returned correction explain the syndrome in the caller's index space. The other hands a decoder one instance under two presentations differing only in bookkeeping, where two feasible corrections of different weight prove the heavier is not minimum-weight. Verdicts are gated on what each library declares, so a firing contradicts a published guarantee. Nine configurations from five public libraries give three results. Documentation answers 4 of 54 capability questions. Bounded-distance correctness, the property callers most depend on, has a direct declaration yield of 0.0%, though its hypotheses hold in 62.1% of cases. Presentation sensitivity is real but shallow. One solver moved to a 26% heavier correction under a different numbering, which reaches the logical class at most once in twenty thousand shots. Established evaluation misses corruptions that preserve logical parity, while one summation over the caller's weights catches every one we injected. All 639 certificates ship as bundles a standalone verifier re-derives from first principles.
Quantum error correction (QEC) enables reliable computation on noisy hardware by encoding logical information across many physical qubits and periodically measuring parities to detect errors. A decoder is the classical algorithm that uses these measurements to infer which error most likely occurred, so that the system can correct it. The decoder's accuracy-how rarely it makes the wrong guess-directly determines the scale of quantum computation that can be reliably executed. With a wealth of competing decoding algorithms, a QEC system designer needs reliable methods to evaluate them. Today, the dominant approach is to evaluate decoders using Monte Carlo simulation. However, simulation has several drawbacks such as requiring many samples to produce low variance estimates.
In this work, we develop a new systematic analysis for evaluating decoders. We introduce a novel formal semantics of a core language for QEC programs that captures the de facto standard Stim circuit format, providing a principled theoretical foundation for the emerging space of fault-tolerant quantum systems design. Given a QEC program and a decoder, our verifier can quantify both the decoder accuracy and the decoder robustness to drift in physical error rate. Our approach has two key components: (i) a structured search over the space of possible errors; and (ii) a constrained polynomial optimization kernel. A thorough empirical evaluation of our approach suggests that it can outperform simulation, especially in low error rate regimes, and that it can be deployed to quantify decoder robustness over an interval of physical error rates.
This preregistration describes a confirmatory study of an upstream conditioning architecture in a quantum error-correction workflow. The project’s purpose is to test whether an intervention applied prior to the primary decoder produces a real and reproducible decoder-relevant effect, remains compatible with more than one downstream decoder family, generates a measurable exposed-observable statistical footprint, and improves or preserves performance across a preregistered regime rather than only at a single operating point. The study is intentionally limited to architecture-level evaluation, with the public claim set confined to exposed observables, frozen transformations, preregistered statistical tests, explicit negative controls, and bounded interpretation rules. The confirmatory design is organized around five preregistered tests: category existence, decoder compatibility, structural footprint, observable statistical signature, and regime robustness. Across these tests, the central comparison is between a baseline control pipeline and a conditioned pipeline in which the upstream intervention is applied while all non-conditioning settings are held fixed. The study uses frozen observables and frozen execution rules, including matched seeds, shot counts, code distances, physical error rates, geometry, and baseline decoder settings, so that any supported effect can be interpreted as evidence about the architecture under test rather than as a byproduct of post hoc tuning. To preserve a clean-room boundary, the registration restricts primary analysis to exposed, decoder-facing quantities only. These include logical failure, an exposed defect-count summary, and an exposed decoder-difficulty proxy, along with a locked scalar error-load construction derived from control-only standardization. The study does not rely on decoder-internal state variables, hidden confidence traces, or implementation-specific internal diagnostics in its primary confirmatory analyses. This structure is intended to let readers evaluate whether the architecture leaves a reproducible footprint in decoder-facing behavior without disclosing reconstruction-level mechanism details. Expected outcomes are defined in confirmatory rather than speculative terms. If the preregistered hypotheses are supported, the study is expected to provide evidence that an upstream conditioning intervention exists as a real architectural category in QEC, acts before the primary decoder, is compatible with downstream decoding, changes decoder-relevant exposed structure, and produces a reproducible observable statistical footprint in logical-failure behavior. If support is absent, mixed, or null, those outcomes will still be recorded under the frozen rules without rescue through post hoc metric changes, reweighting, or reinterpretation. In either case, the expected result of the registration is a bounded, auditable public record of whether this architecture class shows reproducible category-level behavior under a preregistered confirmatory design. The preregistration is not intended to establish a unique mechanism identity, identify a privileged implementation, disclose implementation-specific reconstruction details, or support claims about exact targeting logic, suppression laws, subset-sizing logic, telemetry-governed control, or broader cross-domain theory narratives. Public-facing interpretation is therefore intentionally limited to category validation and exposed-observable behavior. This is meant to support rigorous public evaluation while preserving strict clean-room limits around protected implementation detail.
Quantum error-correcting code (QECC) implementations are hybrid software-control systems: measured syndromes drive decoder dispatch, recovery actions, and logical checks. Existing QECC verification techniques can prove formal obligations, and general quantum testing can expose final failures, but developers still lack a scalable testing workflow that generates concrete faults and explains where a QECC repair path first diverges. This paper presents ConQEC, to our knowledge the first concolic testing framework for QECC implementations. By combining concrete (Pauli) fault replay with symbolic repair-path constraints, ConQEC generates tests that expose not only final logical failures but also fault--syndrome--decoder--recovery (FSDR) diagnostics: the injected fault, observed syndrome, decoder decision, recovery action, oracle result, and earliest divergent stage. Its symbolic encoding of Pauli faults, syndrome predicates, decoder and recovery relations, and oracle checks enables this diagnostic workflow to scale beyond exponentially increasing amplitude-level quantum-state reasoning. We implemented ConQEC and evaluated it on generated source-level QECC families and public QECC artifacts with up to thousands of qubits. ConQEC detects the seeded bug in every experimental case and reports a replay-valid, fault-localizing FSDR witness for each.
Quantum error correction (QEC) underpins fault-tolerant quantum computing, but the circuits that realize QEC codes (encoders, logical state-preparation and gate routines, and syndrome-extraction schedules) are scattered across papers and one-off repositories in incompatible formats, often documented too sparsely to reconstruct or reuse. We present QECirc (https://qecirc.com/), a community-driven, open library that makes QEC circuits Findable, Accessible, Interoperable, and Reusable (FAIR). Each entry links to its underlying code, ships in Stim and OpenQASM with interactive visualizations, and is checked for correctness before publication. In short, where a catalog such as the Error Correction Zoo describes the codes, QECirc provides the concrete circuits that realize them.
Quantum error correction protects quantum information by encoding it in a code described by three numbers: how many physical qubits it uses, how many logical qubits it protects, and the smallest error it cannot detect. The last is an optimum over exponentially many candidates, so it is read off a solver rather than checked. Here we show that code parameters can be certified by a short certificate, a list or a pairing or a symbolic instance, whose correctness the kernel of a proof assistant decides by computation, and whose size is itself a theorem rather than an estimate. Two published code families have distances settled here: the bivariate bicycle code's [[144,12,12]], certified, and the affine-permutation codes printed at [[1152,580,≤12]] and [[2304,1156,≤14]], settled at twelve and fourteen. Eleven code families and thirty-nine parameter sets follow, with nothing beyond three standard axioms trusted and the pipeline's specification step preset to twenty columns.
Test oracles for quantum transpilers typically judge correctness by comparing compiled output against a reference: a statevector, a sampled distribution, or a unitary compared modulo global phase. A companion empirical study measures how often that choice fails. Roughly 28% of merged Qiskit transpiler bug-fixes (95% Wilson CI 19-40%) repair a fault that corrupts layout metadata, global phase, or run-to-run reproducibility while output stays correct: invisible to a black-box output-equivalence oracle by construction. This paper closes that gap with a fault-class-matched, layout-aware, width-tiered oracle family: a layout/permutation contract checker and a contract-level metamorphic relation (MR-1) for the metadata channel, a global-phase tracker for the phase channel, and a determinism runner for reproducibility. Verified from source on nine real, merged Qiskit transpiler regressions (three per channel), the output-equivalence oracle is blind throughout and the matched mechanism fires on every case. A 675-configuration sweep of the contract/metadata invariant finds no false positive. Synthetic mutant families confirm reliability at scale: 1.00 sensitivity and specificity across 36 mutants apiece for the contract/metadata and global-phase channels, and 1.00 sensitivity (95% CI 0.44-1.00) for reproducibility on the three circuits where the mutation is constructible. The contract checker costs two to six orders of magnitude less than a plain output check, the global-phase tracker is comparably cheap within its exact tier, and only the metamorphic relation carries a bounded cost. Ported natively to pytket/tket, the global-phase mechanism transfers cleanly, an identical 1.00/1.00 result with phases recovered to double-precision accuracy, evidence against a Qiskit-specific artifact.