# Design by Contract Framework for Quantum Software

arXiv: https://arxiv.org/abs/2303.17750 · HTML: https://mlsanity.com/paper/2303.17750/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 10 references that are in the map.
- First posted on arXiv 31 Mar 2023.

## Builds on (most cited first, 3 of 3)

- [Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs](https://mlsanity.com/paper/1905.09721/) (2019)
- [A Deductive Verification Framework for Circuit-building Quantum Programs](https://mlsanity.com/paper/2003.05841/) (2020)
- [Proving Quantum Programs Correct](https://mlsanity.com/paper/2010.01240/) (2020)

## Abstract (arXiv)

To realize reliable quantum software, techniques to automatically ensure the quantum software's correctness have recently been investigated. However, they primarily focus on fixed quantum circuits rather than the procedure of building quantum circuits. Despite being a common approach, the correctness of building circuits using different parameters following the same procedure is not guaranteed. To this end, we propose a design-by-contract framework for quantum software. Our framework provides a python-embedded language to write assertions on the input and output states of all quantum circuits built by certain procedures. Additionally, it provides a method to write assertions about the statistical processing of measurement results to ensure the procedure's correctness for obtaining the final result. These assertions are automatically checked using a quantum computer simulator. For evaluation, we implemented our framework and wrote assertions for some widely used quantum algorithms. Consequently, we found that our framework has sufficient expressive power to verify the whole procedure of quantum software.