Welcome to Qbricks

Qbricks is open-source environment for automated formal verification of quantum programs. It enables the writing of quantum circuit building programs, specified with their I/O functions and/or their resource requirements. Thanks to a characterization of quantum circuits as paramatrized path-sums, the specifications of Qbricks circuit-building quantum programs reduces to first-order proof obligations. Its host language, the Why3 deductive verification environment, provides an interface with SMT-solvers, enabling an high-level of automation in the vertfication of Qbricks specifications.

So far, Qbricks framework enabled the verified implementation of several emblematic algorithm from the litterature, including the Deutsch-Jozsa algorithm, Quantum Phase Estimation (QPE), Grover search algorithm and Shor order finding (including an implementation of the oracle).



It is developed at the CEA LIST (part of Université Paris-Saclay) in collaboration with Laboratoire Méthodes Formelles(Université Paris-Saclay).

For an introduction to Qbricks, please read our article and see the related presentation slides. A tutorial redaction is under progress.


PostDoc open position (2 years) : verified compilation

The goal of this post-doctoral position is to extend formal verification practice to quantum compilation. Possibilities include, among others, error correction mechanisms in certified quantum code, together with specifications and reasoning technique for certifying its reliability, automatized certified optimizer for quantum circuits, hardware agnostic assembly language together with its compiler,

Keywords: quantum programming, compilation, optimization, formal verification

How to apply

Applications should be sent to christophe.chareton@cea.fr as soon as possible (first come, first served) and by early July 2021 at the latest. Candidates should send a CV, a cover letter, a transcript of all their university results, as well as contact information of two references. Each position is expected to start in October 2021.

Advisors: Christophe Chareton (CEA), Sébastien Bardin (CEA) Contact: christophe.chareton@cea.fr



Name Position Affiliation Web site
Sébastien Bardin Senior CEA LIST, Université Paris-Saclay Sébastien Bardin
Benoît Valiron Senior LMF, Université Paris-Saclay Benoît Valiron
Christophe Chareton Junior CEA LIST, Université Paris-Saclay Christophe Chareton
Jérôme Ricciardi PhD student CEA LIST, Université Paris-Saclay Jérôme Ricciardi
Tomas Barros Carneiro Intern CEA LIST, Université Paris-Saclay Tomas Barros Carneiro
Mohamed Bassiouny Intern CEA LIST, Université Paris-Saclay Mohamed Bassiouny


International conference



Short articles