VeriQ AncillaGuard

VeriQ AncillaGuard verifies whether a unitary Qiskit circuit restores selected dirty ancilla qubits for every possible input state. Unsafe targets are diagnosed as logic errors, phase errors, or both. Ancilla-local violations can also be repaired with a short sequence of single-qubit rotations.

The implementation accompanies the paper Formal Verification of Quantum Ancilla Safety. It provides two complementary verification backends:

• MQT QCEC, an equivalence-checking backend that works out of the box.
• Quokka-Sharp, the weighted-model-counting backend used by the paper.

This experimental 0.1 release intentionally bundles the paper-era Quokka-Sharp implementation. Migrating to the current upstream PyPI package is planned separately so that the validated research kernel remains stable.

Installation

VeriQ AncillaGuard requires Python 3.10 or newer and Qiskit 2.x.

python -m pip install veriq-ancillaguard

To install the latest source instead:

git clone https://github.com/veriq-toolkit/Ancilla-Safety.git
cd Ancilla-Safety
python -m pip install .

MQT QCEC is installed automatically. The Quokka backend additionally requires an executable GPMC weighted model counter. Point the package to it with either an argument or an environment variable:

export GPMC_PATH=/path/to/gpmc

The repository includes the pinned GPMC source under third_party/GPMC for reproducible Linux builds. Its build prerequisites are CMake, GMP, MPFR, zlib, and a C++ compiler.

Optional Docker Image

Docker is not required for the Python package. It is provided as a reproducible Linux environment that builds the pinned GPMC source and makes both backends available without a separate solver installation:

docker build -t veriq-ancillaguard .
docker run --rm veriq-ancillaguard --help
docker run --rm -v "$PWD:/data:ro" veriq-ancillaguard \
  verify /data/circuit.qasm --ancilla 0 --backend quokka

Installation Check

Run a built-in safe case and a known logic-error case after installation:

ancillaguard self-test

QCEC is always checked. Quokka is also checked when GPMC is available and is otherwise reported as skipped. To require a specific backend:

ancillaguard self-test --backend qcec
ancillaguard self-test --backend quokka --gpmc /path/to/gpmc

Quick Start

from qiskit import QuantumCircuit
from veriq_ancillaguard import verify_dirty_safety

circuit = QuantumCircuit(2)
circuit.cx(0, 1)
circuit.cx(0, 1)

result = verify_dirty_safety(
    circuit,
    ancillas=[circuit.qubits[1]],
    backend="qcec",
)

print(result.status)                  # SafetyStatus.SAFE
print(result.targets[0].logic_safe)  # True
print(result.targets[0].phase_safe)  # True

Targets may be Qiskit Qubit objects or global integer indices. Targets must be provided explicitly; the package never guesses which register contains ancillas.

To use Quokka-Sharp:

result = verify_dirty_safety(
    circuit,
    ancillas=[1],
    backend="quokka",
    gpmc_path="/path/to/gpmc",
)

Repair

The repair pipeline handles violations that remain local to an ancilla qubit. It returns a new circuit and leaves the input circuit unchanged.

from qiskit import QuantumCircuit
from veriq_ancillaguard import repair_dirty_safety

circuit = QuantumCircuit(1)
circuit.z(0)

result = repair_dirty_safety(circuit, ancillas=[0])
repaired = result.circuit

print(result.before.status)  # SafetyStatus.UNSAFE
print(result.after.status)   # SafetyStatus.SAFE
print(result.patches[0].angles)

Repair uses the Quokka backend and therefore requires GPMC. If an error leaves the ancilla entangled or correlated with other qubits, a local repair is not possible and the result reports the failure rather than changing unrelated qubits.

Command Line

OpenQASM 2 files can be checked without writing Python:

ancillaguard verify circuit.qasm --ancilla 'anc[0]' --backend qcec
ancillaguard verify circuit.qasm --ancilla 3 --backend quokka --gpmc /path/to/gpmc
ancillaguard repair circuit.qasm repaired.qasm --ancilla 'anc[0]' --gpmc /path/to/gpmc

Commands print JSON results and return a nonzero exit code when verification does not establish safety.

Benchmark Examples

Four OpenQASM 2 examples are included under examples/benchmarks. Each checks one documented ancilla target and is expected to be safe with both backends. Run all examples from a source checkout:

python examples/run_benchmarks.py --backend qcec
python examples/run_benchmarks.py --backend both --gpmc /path/to/gpmc

The large GHZ example contains 1399 qubits and is intended to demonstrate the backend workflow, not to define a portable performance baseline.

Supported Circuits

The framework currently targets purely unitary circuits. Measurements, resets, delays, classical control flow, and unbound parameters are rejected.

The frozen Quokka backend accepts the following basis instructions:

id, x, y, z, h, s, sdg, t, tdg,
rx, ry, rz, cx, cz, cs, csdg, ccx

Transpile other unitary instructions explicitly before invoking Quokka. The package does not silently transpile user circuits because preserving the exact verification boundary is important.

Result Semantics

For every selected ancilla, the verifier checks commutativity against Pauli-Z and Pauli-X:

• failed Z check: ErrorKind.LOGIC
• failed X check: ErrorKind.PHASE
• both checks pass: the target is dirty safe
• backend cannot decide: SafetyStatus.INCONCLUSIVE

MQT QCEC's equivalent_up_to_global_phase result is a failed commutativity check here. A non-trivial relative global phase between U and P U P is an anti-commutation witness, not a successful exact equality.

Development

python -m pip install -e '.[dev]'
pytest
ruff check src tests examples
python -m build
python -m twine check dist/*

Quokka integration tests run when GPMC_PATH is configured; otherwise they are skipped. See CONTRIBUTING.md for the contribution workflow.

Provenance and Citation

The bundled research backend is pinned to Quokka-Sharp commit 9131a8eab786ffe983a77af6bb374ffdeab06dc4. Detailed third-party provenance is recorded in NOTICE.md. Citation metadata is available in CITATION.cff.

The original artifact-evaluation package and experimental outputs are archived separately at Zenodo. The paper used the former repository URL Veri-Q/Ancilla-Safety. GitHub redirects that transferred-repository URL to the canonical repository above. The software is published under the product name VeriQ AncillaGuard while the repository retains its original name for continuity with the paper.

License

VeriQ AncillaGuard, the bundled Quokka-Sharp snapshot, and the vendored GPMC source are available under the MIT License. See LICENSE and NOTICE.md.