# Relational Proofs for Quantum Programs

## TL;DR

This paper introduces a relational program logic for quantum programs, enabling verification of complex properties like security, reliability, and equivalence in quantum computing, based on a novel quantum analogue of probabilistic couplings.

## Contribution

It presents a new relational logic framework for quantum programs, expanding verification capabilities for quantum security, teleportation, and quantum walk equivalences.

## Key findings

- Verified uniformity in quantum Bernoulli factory samples
- Assessed reliability of quantum teleportation under noise
- Proved security of quantum one-time pad and quantum walk equivalence

## Abstract

Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), security of quantum one-time pad and equivalence of quantum walks.