QECV: Quantum Error Correction Verification

TL;DR

QECV is a verification framework for stabilizer quantum error correction codes, combining a specialized language, assertion system, and Hoare logic to ensure correctness efficiently, demonstrated through complexity analysis and case studies.

Contribution

It introduces QECV, a novel framework with a dedicated language, assertion system, and proof rules for verifying stabilizer QEC codes' correctness.

Findings

QECV effectively verifies stabilizer codes.

The framework is supported by theoretical complexity analysis.

Case studies validate QECV on repetition and surface codes.

Abstract

Quantum Error Correction (QEC) is essential for fault-tolerant quantum copmutation, and its implementation is a very sophisticated process involving both quantum and classical hardware. Formulating and verifying the decomposition of logical operations into physical ones is a challenge in itself. In this paper, we propose QECV, a verification framework that can efficiently verify the formal correctness of stabilizer codes, arguably the most important class of QEC codes. QECV first comes with a concise language, QECV-Lang, where stabilizers are treated as a first-class object, to represent QEC programs. Stabilizers are also used as predicates in our new assertion language, QECV-Assn, as logical and arithmetic operations of stabilizers can be naturally defined. We derive a sound quantum Hoare logic proof system with a set of inference rules for QECV to efficiently reason about the correctness of QEC programs. We demonstrate the effectiveness of QECV with both theoretical complexity analysis and in-depth case studies of two well-known stabilizer QEC codes, the repetition code and the surface code.