quantum-fault-tolerance-verification - SKILL.md Agent Skill

name: quantum-fault-tolerance-verification description: "Quantum fault-tolerance verification methodology using symbolic execution for quantum error correction codes. Formal verification framework for proving fault-tolerance properties of QECC implementations. Use when analyzing quantum error correction, verifying fault-tolerance properties, or implementing quantum programs. Activation: quantum fault tolerance, QECC verification, quantum error correction, quantum symbolic execution."

Quantum Fault-Tolerance Verification

Formal verification framework for quantum error correction codes (QECC) using quantum symbolic execution techniques. Enables automatic verification of fault-tolerance properties in quantum programs.

Overview

This methodology addresses the challenge of verifying fault-tolerance in quantum error correction codes:

Manual proofs are impractical for complex QECCs due to vast error combinations
Experimental verification is limited by physical constraints
Provides automatic formal verification using quantum symbolic execution
Evaluated on universal set of logical operations across different QECCs

Core Concepts

Quantum Fault-Tolerance

A QECC is fault-tolerant if it can correct errors even when physical operations are themselves noisy.

Definition: A QECC implementation is fault-tolerant if for any input state |ψ⟩ and any correctable error set E:

E_corr ∘ E ∘ U = U ∘ E' ∘ E_corr

Where:

U is the logical operation
E is physical error
E_corr is error correction
E' is transformed error (still correctable)

Quantum Symbolic Execution

Extends classical symbolic execution to quantum programs:

Symbolic quantum states: Represent states with symbolic amplitudes
Path exploration: Explore all possible error paths
Constraint generation: Generate verification conditions for fault-tolerance

Methodology

1. Quantum Program Formalization

Program Syntax

Program ::= Operation ; Program | ε
Operation ::= Unitary(U) | Measure | ErrorChannel(E)
U ::= H | CNOT | T | S | etc.
E ::= Pauli(X, Y, Z) | Depolarizing | etc.

Denotational Semantics

[[Unitary(U)]](|ψ⟩) = U|ψ⟩
[[Measure]](|ψ⟩) = Σᵢ Mᵢ|ψ⟩⟨ψ|Mᵢ†
[[ErrorChannel]](|ψ⟩) = Σₖ Eₖ|ψ⟩⟨ψ|Eₖ†

2. Fault-Tolerance Verification Algorithm

def verify_fault_tolerance(program, qecc, max_errors):
    """
    Verify fault-tolerance of QECC implementation
    
    Args:
        program: Quantum program to verify
        qecc: Error correction code specification
        max_errors: Maximum error weight to consider
    
    Returns:
        (is_fault_tolerant, counterexample) or proof
    """
    
    # Step 1: Generate symbolic execution tree
    tree = generate_symbolic_tree(program, max_errors)
    
    # Step 2: Apply error propagation
    for path in tree.paths:
        propagate_errors(path, qecc)
    
    # Step 3: Check fault-tolerance condition
    for path in tree.paths:
        if not check_fault_tolerance_condition(path, qecc):
            return False, path.counterexample
    
    # Step 4: Generate proof
    return True, generate_proof(tree)

def generate_symbolic_tree(program, max_errors):
    """Generate symbolic execution tree with error branches"""
    tree = ExecutionTree()
    current = tree.root
    
    for op in program:
        if op.type == "ErrorChannel":
            # Branch for each possible error
            for error in generate_errors(op, max_errors):
                current.add_branch(error)
        else:
            current = current.add_node(op)
    
    return tree

def propagate_errors(path, qecc):
    """Propagate errors through quantum circuit"""
    # Track error operators through Clifford operations
    # Apply commutation relations
    # Update syndrome measurements
    pass

def check_fault_tolerance_condition(path, qecc):
    """Verify fault-tolerance condition for execution path"""
    # Check: errors remain within correctable set
    # Check: logical operations commute with errors
    # Check: syndrome extraction is correct
    pass

3. Symbolic Quantum State Representation

class SymbolicQuantumState:
    def __init__(self, n_qubits):
        self.n = n_qubits
        self.amplitudes = {}  # Symbolic amplitudes
        self.errors = []       # Tracked error operators
    
    def apply_unitary(self, U):
        """Apply unitary operation symbolically"""
        for e in self.errors:
            # Conjugate error: U e U†
            e = self.conjugate_error(U, e)
        return self
    
    def apply_error(self, error):
        """Add error operator"""
        self.errors.append(error)
    
    def measure(self, basis):
        """Symbolic measurement"""
        # Track measurement outcomes symbolically
        # Update post-measurement state
        pass

Verification Workflow

Step 1: Encode QECC Specification

from quantum_verification import QECC

# Define surface code
surface_code = QECC(
    name="Surface Code",
    distance=3,
    stabilizers=[
        "X1 X2 X3 X4",
        "Z1 Z2 Z3 Z4",
        # ...
    ],
    logical_ops={
        "X_L": "X1 X2 X3",
        "Z_L": "Z1 Z4"
    }
)

Step 2: Define Quantum Program

program = QuantumProgram([
    PrepareLogical(|0⟩),
    ApplyTransversal(H),
    MeasureLogical(Z),
])

Step 3: Run Verification

result = verify_fault_tolerance(
    program,
    surface_code,
    max_errors=1  # Single error fault-tolerance
)

if result.is_fault_tolerant:
    print("QECC is fault-tolerant!")
    print("Proof:", result.proof)
else:
    print("Fault-tolerance violated!")
    print("Counterexample:", result.counterexample)

Supported QECC Types

1. Stabilizer Codes

Surface codes
Color codes
Shor code
Steane code
Rotated surface codes

2. Subsystem Codes

Bacon-Shor code
Subsystem surface codes

3. Floquet Codes

Honeycomb codes
Floquet surface codes

Logical Operations Verified

Universal Gate Set

Clifford Group: H, S, CNOT
T Gate: Magic state distillation and injection
Measurements: Pauli measurements
State Preparation: |0⟩, |+⟩, |T⟩

Fault-Tolerance Criteria

Preparation: Errors don't spread to logical space
Gates: Errors don't propagate to uncorrectable weight
Measurement: Errors don't corrupt measurement outcomes
Syndrome: Errors are correctly identified and located

Error Models

1. Pauli Errors

class PauliErrorModel:
    def __init__(self, px, py, pz):
        self.px = px  # X error probability
        self.py = py  # Y error probability
        self.pz = pz  # Z error probability

2. Depolarizing Channel

class DepolarizingModel:
    def __init__(self, p):
        self.p = p  # Total depolarizing probability
        self.components = [I, X, Y, Z]  # Equally likely

3. Coherent Errors

class CoherentError:
    def __init__(self, rotation_angle, axis):
        self.angle = rotation_angle
        self.axis = axis

Advanced Techniques

Quantum Abstract Interpretation

Abstract domains for efficient verification:

Pauli abstract domain: Track Pauli errors only
Stabilizer abstract domain: Track stabilizer group membership
Error weight domain: Track error weight bounds

Compositional Verification

def verify_compositionally(subroutines, glue_logic):
    """Verify by composing verified subroutines"""
    contracts = []
    for sub in subroutines:
        contracts.append(verify_subroutine(sub))
    
    # Verify glue logic preserves contracts
    return verify_glue(contracts, glue_logic)

Parameterized Verification

Handle families of QECCs:

Distance-d surface codes
Code concatenation
Variable code parameters

Implementation Details

Tool Architecture

QECC Verifier
├── Parser: Parse quantum programs (OpenQASM, Quipper)
├── Symbolic Engine: Symbolic execution
├── Error Propagator: Track error evolution
├── Checker: Fault-tolerance verification
└── Proof Generator: Output proofs/counterexamples

Supported Input Formats

OpenQASM 2.0/3.0
Quipper
Custom DSL
Direct API

Output

Verification result (pass/fail)
Counterexample traces (if fail)
Proof certificates (if pass)
Statistics

Limitations

Scalability: Exponential in code distance
Error Model: Limited to certain error types
Gate Set: Universal set verification is expensive
Resource: Large memory for complex codes

Usage Example

from quantum_verification import *

# Load surface code
surface_code = load_qecc("surface_code_d3.json")

# Define logical CNOT
program = Program()
program.add(PrepareLogical([|0⟩, |0⟩]))
program.add(TransversalCNOT())
program.add(MeasureLogical([Z, Z]))

# Verify
result = verify(program, surface_code, 
              max_errors=1, 
              error_model=Depolarizing(p=0.01))

print(result)
# Output: 
# Fault-Tolerant: True
# Proof size: 1243 steps
# Runtime: 45.2s

References

Chen et al., "Verifying Fault-Tolerance of Quantum Error Correction Codes", arXiv:2501.14380
Gottesman, "Stabilizer Codes and Quantum Error Correction", arXiv:quant-ph/9705052
Fowler et al., "Surface Codes: Towards Practical Large-Scale Quantum Computation", arXiv:1208.0928
Aaronson & Gottesman, "Improved Simulation of Stabilizer Circuits", arXiv:quant-ph/0406196

Related Skills

quantum-error-correction
quantum-circuit-synthesis
quantum-abstract-interpretation
quantum-program-verification