Formal Verification of Quantum Stabilizer Code
summary
Formalization in Coq of the stabilizer-group algebra and an n‑qubit Pauli/phase construction yields proved algebraic properties (eigenvalues, generators) and a verified 4‑qubit stabilizer code via density‑matrix semantics, but full density‑matrix proofs hit exponential blowup. The project uses squire automation for some proofs, reports that the stabilizer formalism avoids 2^n state reasoning, and aims to produce a generalized stabilizer encoder and scalable verification pipeline; work is partial but the small examples succeed.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:48Quantum programs need verification
- 3:15Formal methods in quantum computing
- 5:22Verifying a simple quantum program
- 7:11Quantum error correction overview
- 10:00Density matrix challenges
- 12:11Stabilizer formalism
- 13:38Research goals and progress
- 15:45Contributions and future
- 16:56Q&A
related talks
01h 04mLearning Beyond Stabilizer States
19mAll Together Now! Programming the Quantum Computer
59mQuantum Physics for Software Developers
47mQuantum Computing and You
41mQuantum Computing Deep Dive
48mGetting Started with Quantum Programming
01h 03mReal Quantum Computing
54mThe Present and Possible Future of Quantum Computing