Quantum acceleration is about to become a reality of the computing industry. However, it remains unclear how to gauge quantum program correctness. Indeed, in the general case the only way to extract useful information from the state of a quantum system is through quantum measurement, which collapses this state and impedes further execution on it. Therefore, read-only debugging along runtime is impossible.

As a result, formal methods and static analysis are likely to play a decisive role in future quantum software engineering.

In this tutorial we propose an introduction to the field of quantum formal verification, its main motivations and challenges, and a focus an a case solution: Qbricks

It will be structured as such : 1. a generic introduction to quantum programming and its specifities: the hybrid model and the interplay between (i) classical control and instructions (ii) quantum calculi, with a clear focus on the verification problem, – 30min 2. the principles of formal verification and the requirements to be met by a formal solution to the quantum verification problem, – 30min 3. a synthetic presentation of the solution we develop in our lab : Qbricks. This principally aims at illustrating a case implementation for the required material identified in 2, – 30 min 4. a “hands-on” session, including some Qbricks development from participants, Bell state preparation (quantum hello world) to a standard full algorithm - 1 h.

The expected outcomes are to give attendees a generic view on - quantum programming and the main problems a quantum programmer will encounter, - the possibilities to represent potentially exponentially large quantum state descriptions in a compact formally tractable manner, - human-machine interactive correctness proof for quantum programs