Prerequisites: Strong programming skills; ideally familiarity with quantum computing fundamentals; interest in programming languages and/or formal verification. Experience with proof assistants (ideally Rocq) is a plus, but not required.
Description: Quantum error correction (QEC) is essential for building reliable quantum computers, but the correctness of QEC protocols is notoriously difficult to reason about. Stabiliser codes, including the widely studied surface codes and colour codes, are among the most promising approaches to fault-tolerant quantum computing, yet the tools for formally verifying that these codes behave as intended remain underdeveloped.
Currently, quantum error correction verification is used to verify the correctness of error-correction algorithms, assuming virtual qubit layouts. However, error correction applications rely on the assumption of low-level qubit topological information, such as qubit layout and connectivity. The verification of any error correction algorithms should be based on the topological information with error models, to guarantee that the error rates of qubits and gates are within a reasonable bound. Such example error correction algorithms include surface and colour codes. On the other hand, quantum error correction algorithms typically use a restricted gateset, which enables effective simulation and verification. We intend to develop an automated verification framework to ensure the correctness of quantum error correction with topological information.
This project builds on our group’s prior work on Pqasm, a verified framework for reasoning about quantum state preparation programs, and Qafny, a type-guided approach to quantum program verification. The core idea is to extend these foundations in two directions:
(1) Stabiliser-based reasoning. Rather than tracking full quantum states, stabiliser formalism offers a compact, algebraically tractable representation of an important class of quantum states. The project will develop a program logic or type system that operates over stabiliser tableaux, enabling efficient automated reasoning about stabiliser circuits. See https://pennylane.ai/qml/demos/tutorial_stabilizer_codes
(2) Topological connectivity. Real QEC codes, surface codes, toric codes, and their variants, have a natural graph-theoretic structure that constrains which physical qubits interact. By incorporating this topological connectivity information into the verification framework, we can check not only logical correctness but also that a QEC protocol is implementable on a given hardware topology, and that syndrome extraction and decoding respect the code’s geometric structure. See https://www.quera.com/glossary/syndrome-extraction
The student will design and implement a verification tool (likely embedded in Rocq) that combines stabiliser reasoning with topological graph structure, and evaluate it on a selection of QEC protocols such as Steane’s 7-qubit code, the rotated surface code, or the colour code.
Expected Outcomes:
- A formal model linking stabiliser tableaux to a program logic suitable for QEC verification
- Integration of topological/connectivity constraints into the reasoning framework
- Mechanised proofs of correctness for at least one standard QEC protocol
- A written thesis documenting the design, implementation, and evaluation
Related Publications:
- https://arxiv.org/abs/2501.05616
- https://arxiv.org/abs/1311.0277
- https://dl.acm.org/doi/10.1145/3763157