Building a trustworthy quantum era through formal verification

Laboratory on Formal Methods for Quantum Computing
Senior Lecturer：DO Minh Canh

E-mail：
［Research areas］
Formal Methods, Quantum Computing
［Keywords］
Formal Specification, Model Checking, Theorem Proving, Quantum Computation, Quantum Information

Skills and background we are looking for in prospective students

We welcome highly motivated students with an interest in formal methods and quantum computing, a good knowledge of mathematics (especially mathematical logic and linear algebra), and strong programming skills (C⁺⁺, Java, Python).

What you can expect to learn in this laboratory

In our laboratory, students will learn how to formalize quantum systems as state machines; how to specify state machines in a formal specification language, such as Maude or CafeOBJ; and how to formally verify that state machines enjoy desired properties using model checking and/or theorem proving techniques. Through these research activities, students are expected to acquire a solid theoretical foundation, advanced practical skills, and a passion for advancing both conventional and quantum technologies in ways that benefit society.

【Job category of graduates】 Researcher & Engineer

Research outline

With recent exponential investments from governments and major companies, building large-scale quantum computers capable of running advanced algorithms, such as Shor’s algorithm for effectively solving the factoring and discrete logarithm problems, is becoming increasingly feasible. Despite its promise, quantum computing is fundamentally different from classical computing because it relies on principles of quantum mechanics that are often counterintuitive, making it challenging to design and implement quantum systems accurately. Moreover, traditional testing techniques are much less effective for quantum systems due to the nondeterminism and probabilistic outcomes of quantum measurement. Thus, formal verification is essential to ensure their correctness before they can be trusted in practice. Our research focuses on formal methods for quantum computing, including but not limited to the following research topics.

An algebraic specification for quantum computation

Symbolic and exact reasoning about quantum computation is essential for formal verification, and algebraic approaches provide a promising direction for achieving this goal. This research develops an algebraic specification framework for modeling and reasoning about quantum computation. In particular, we use the ring D[ω] to represent complex numbers exactly; use Dirac notation to model quantum states and operations; and leverage a set of laws from quantum mechanics and basis matrix operations expressed in Dirac notation to automate reasoning about quantum computation. This algebraic specification for quantum computation is expected to serve as a foundational formal framework upon which other formal verification techniques can be developed.

A unified, expressive, and scalable framework for formal specification and verification of quantum systems

System specification and property specification are necessary inputs for formal verification techniques to determine whether a system satisfies desired properties. This research develops a powerful formal specification language capable of modeling a wide range of quantum systems, including those with concurrency and communication, together with scalable formal verification techniques from model checking to theorem proving.
In particular, we introduce Concurrent Dynamic Quantum Logic as a logical framework for modelling concurrent behavior and communication among participants. Based on the algebraic specification for quantum computation and some optimization techniques, the verification process can be automated and can effectively manage the large number of interleavings arising from concurrency and communication.

A verifiable recursive quantum programming language with formal semantics 

Procedures and recursion are fundamental features for structuring programs in a modular and scalable way. This research develops a recursive quantum programming language that supports modular design of quantum systems and enables their rigorous verification using formal methods grounded in its formal semantics, while preserving the unique advantages of quantum computing. In particular, we introduce the syntax and operational semantics of the language to support all basic constructs and recursive procedure calls. Based on its semantics, we develop a framework for specifying quantum programs and verifying their correctness automatically.

Key publications

1. Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata. “Parallel Maude-NPA for Cryptographic Protocol Analysis”, IEEE Transactions on Dependable and Secure Computing, 12(6): 6714-6731, IEEE, 2025.
2. Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata. “Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic”, ACM Transactions on Software Engineering and Methodology, 34(6): 1-36, ACM, 2025.
3. Canh Minh Do, Yati Phyo, Adrián Riesco, Kazuhiro Ogata. “Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way”, ACM Transactions on Software Engineering and Methodology, 32(6): 1-38, ACM, 2023.

Equipment

Maude (a rewriting logic-based specification/programming language)
CafeOBJ (an advanced formal specification and verification language)
MacPros (a high-performance computing environment for experiments)