Building trust in the future of quantum computing

A trio of researchers at the Japan Advanced Institute of Science and Technology has published what they claim is a significant step forward in formally verifying quantum protocols before those protocols are deployed in the real world. Their paper, published December 12 in ACM Transactions on Software Engineering and Methodology, introduces Concurrent Dynamic Quantum Logic, or CDQL — an extension of an earlier formalism called Basic Dynamic Quantum Logic that could not handle the concurrent actions that real quantum systems require.

The paper, by Assistant Professor Canh Minh Do, Associate Professor Tsubasa Takagi, and Professor Kazuhiro Ogata, sits at an unglamorous but increasingly important intersection: quantum software reliability. As quantum hardware from IBM, Google, and others scales toward practical relevance, the question of whether the software running on it can be trusted is no longer theoretical. Quantum communication and cryptography are already in commercial use. The formal methods community wants to make sure they are correct before they are everywhere.

The core problem is that quantum systems behave differently from classical ones. Measuring a qubit collapses its state — and that measurement changes the system. Classical testing techniques, which run a program and check the output, do not work well when the output can be different every time you look. Formal methods — mathematical specification and verification of system behavior — are the alternative.

BDQL, the researchers earlier framework, could handle sequential quantum operations but could not model multiple participants acting simultaneously in a protocol. Real quantum communication involves exactly that kind of concurrency: two or more parties exchanging information at the same time. CDQL extends BDQL to capture those interactions. The paper also provides a transformation from CDQL models back to BDQL models, maintaining compatibility with the earlier semantics.

The technical contribution that may matter most for practicality is the lazy rewriting strategy. When verifying concurrent systems, the number of possible interleavings of actions grows combinatorially — a known scalability killer for model checking. The lazy rewriting strategy eliminates irrelevant interleavings from earlier stages of the verification process and reuses results to avoid recomputation. The claim is that this makes verification faster and more tractable for real-world protocols.

The CDQL framework has a known gap: it cannot handle quantum data sharing over quantum channels. The authors say they plan to address this in future work.

Do own estimate for impact is cautious — five to ten years for meaningful contribution to reliable quantum communication and cryptography. That is a more measured claim than the usual quantum hype, and it is worth taking at face value. Formal verification of quantum systems is hard, the tools are immature, and the hardware is still noisy. The research is real; the timeline should be taken with the usual skepticism.

Funding for the work came from JAIST fundamental research grant, JST SICORP, and several JSPS KAKENHI grants. The Springer version of the earlier BDQL-based verification work is available as Automated Quantum Program Verification in Dynamic Quantum Logic in the 2023 rewriting logic proceedings.

The broader context is a field waking up to the fact that quantum software is software, with all the bugs and correctness problems that implies. IBM quantum error correction pipelines, Google surface code demonstrations, the various quantum networking testbeds under development — none of them get a pass on correctness because the hardware is quantum. Whether CDQL specifically becomes a widely adopted formalism remains to be seen, but the problem it addresses is genuine and not going away.

Paper: Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic — ACM Transactions on Software Engineering and Methodology, DOI 10.1145/3708475

Authors: Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata (JAIST)

Funding: JAIST Research Grant for Fundamental Research, JST SICORP Grant JPMJSC20C2, JSPS KAKENHI Grants JP22J23575, JP23K28060, JP23K19959, JP24K20757, JP24KK0185, JP24K23858