Verification of Nondeterministic Quantum Programs

A nondeterministic program is one that says do this or that without pinning down which — a way to write a specification and its possible implementations in the same language, and to model unknown behaviour like an unknown hardware error — but quantum programs, whose states are density operators and whose assertions are not true-or-false but numerical expectations, had a theory only for whether such programs terminate, not for whether they are correct; this work from the University of Technology Sydney builds a full Hoare logic for nondeterministic quantum programs, proves it sound and relatively complete, uses it to prove a quantum error-correction scheme and other algorithms correct, and ships a Python proof assistant that automates the routine matrix work.

The argument in one glance

Problem

Nondeterministic quantum programs could be checked for halting, not correctness

A nondeterministic program contains a choice — do this or that — with no rule for which branch is taken. It is a powerful idea: it lets you write an abstract specification and its concrete implementations in one language and refine one into the other, and it lets you model behaviour you do not control, such as which of several errors a noisy quantum channel introduced. Nondeterminism has existed in quantum programming for years, but the formal theory only answered whether such a program terminates. Whether it actually computes the right answer — verification — was essentially unaddressed.
What people did

Borrow Hoare logic, the classical way to prove programs correct

For ordinary programs there is a mature answer: Hoare logic. You annotate a program with a precondition and a postcondition, and a set of syntax-directed proof rules lets you derive, step by step, that if the precondition holds before running, the postcondition holds after. It is modular and it is the foundation of program verification. There is already a Hoare logic for deterministic quantum programs to build on.
Why it fell short

Quantum breaks the classical mould, and nondeterminism compounds it

Quantum programs do not fit classical Hoare logic. Their state is not a set of variables but a density operator on a Hilbert space; their operations are super-operators, including measurements that disturb the state; and an assertion is not true-or-false but a Hermitian operator, whose satisfaction by a state is a number between zero and one, an expectation. Nondeterminism piles on: a program no longer has one behaviour but many, one per way the choices resolve, and correctness has to hold across all of them at once. No proof system covered this combination.
This paper's idea

A sound, complete Hoare logic for nondeterministic quantum programs

The paper gives the missing theory. It defines the meaning of a nondeterministic quantum program as the set of all behaviours its choices can produce, then defines partial and total correctness against rich assertions built from Hermitian operators, taking the worst case over the nondeterministic choices. On top of this it builds Hoare-style proof rules, proves them both sound and relatively complete, uses them by hand to prove a quantum error-correction scheme and other algorithms correct, and implements a Python proof assistant that automates the tedious matrix manipulations.

Why this problem is worth solving

The construct at the heart of the paper is worth understanding in its own right.

Nondeterministic choice is a program construct that offers a choice between two behaviours — do this or that — without any rule saying which is taken. That vagueness is deliberately useful. It lets a single language express both a specification, which says only what should happen, and an implementation, which says exactly how, so a developer can start from an abstract program and refine it step by step into a concrete one, checking correctness at each stage before the details are filled in and catching errors early. It also models things a program does not control: a noisy channel that may flip one of several bits, an environment that may behave in any of several ways. When the choice is treated as demonic — adversarial — a program is only correct if it does the right thing no matter how the choices are resolved, which is exactly the guarantee you want when the choice represents an unknown error or a hostile world.

Making this work for quantum programs means confronting how differently they are built.

In a classical program, an assertion is a logical predicate that is either true or false in a given state, and Hoare logic reasons about how those truths flow through the code. Quantum programs upend every piece of this. A program state is a density operator, a mathematical object describing a possibly-mixed quantum state over a Hilbert space; the operations are super-operators, the general form of a quantum step, which includes measurements that unavoidably disturb the state they read. Most strikingly, a quantum assertion is not true-or-false at all. It is a Hermitian operator — an observable — and the degree to which a state satisfies it is a number between zero and one, the expectation you would get by measuring that observable. So the identity operator plays the role of true and the zero operator the role of false, but everything in between is a partial, quantitative degree of satisfaction. A verification theory for quantum programs must be built on this quantitative, operator-valued notion of assertion from the ground up.

What people did before, and where it broke

Classical Hoare logic. Prove ordinary programs correct with preconditions, postconditions, and syntax-directed rules. Where it broke. It assumes states are variable assignments and assertions are true-or-false, neither of which holds for quantum programs, whose states are density operators and whose assertions are quantitative observables.
Hoare logic for deterministic quantum programs. Prior work lifted Hoare logic to quantum, using Hermitian-operator assertions and expectation-based satisfaction. Where it broke. It handles only deterministic programs — one behaviour each — with no construct for choosing between behaviours, so it cannot reason about a program that models an unknown error or an unrefined specification.
Termination analysis of nondeterministic quantum programs. Earlier work modelled such programs as sets of quantum processes and asked whether they halt, even under demonic and angelic choices, using ranking-style arguments. Where it broke. Termination is only one property. Knowing a program eventually stops says nothing about whether it stops in the right state, which is what verifying an error-correction scheme or an algorithm actually requires.
Interactive theorem provers for quantum programs (CoqQ, QHLProver). Encode a deterministic quantum Hoare logic inside Coq or Isabelle, with machine-checked soundness and support for symbolic qubit counts. Where it broke. They too cover only deterministic programs, and they demand deep proof-assistant expertise, so a nondeterministic program simply cannot be stated, let alone verified, in them.
The gap. Nondeterminism is exactly the tool for modelling unknown errors and unimplemented specifications, and it is exactly where a quantum program stops having a single behaviour — yet the quantum verification theory had been developed only for deterministic programs and, for nondeterministic ones, only for termination. What was missing was a full correctness logic for nondeterministic quantum programs, proven sound and complete, that could actually prove an algorithm right across all the ways its choices might play out.

How the framework works

From a nondeterministic quantum program to a machine-aided proof

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Make a nondeterministic program mean the set of everything it could do, and demand correctness of all of it. The first move is to decide what a program that says do this or that even means. The paper defines the meaning of a nondeterministic quantum program as the whole set of behaviours its choices can produce — resolve the choices one way and you get one behaviour, another way and you get another, and the program is all of them at once. Correctness is then defined against the worst case over that set: a nondeterministic error-correction scheme is correct only if it restores the right state for every possible error the choice could stand for, not just some. Treating the nondeterministic choice as a demonic adversary and certifying the program against the worst outcome it could force is the same worst-case discipline the dynamic-partitioning-leakage work covered elsewhere on this site adopts, bounding a system by imagining the most capable adversary rather than an average or lucky case. This is exactly why the construct is the right way to model an unknown error: proving correctness over all resolutions proves it against whichever error actually occurs.

Rebuild Hoare logic on quantum assertions, where truth is a number. Classical Hoare logic assumes assertions are true or false and flows those truths through the program; none of that survives the move to quantum, where an assertion is an observable and its satisfaction is an expectation between zero and one, and where a measurement in the code disturbs the very state being reasoned about. So the paper reconstructs the whole apparatus for this quantitative world: a rule for each construct, with the measurement rule combining the branches through the measurement operators, the loop rule carrying a quantum invariant, and the choice rule insisting the precondition suffice for both branches. Building a rigorous proof system natively for a domain where the classical logical primitives do not apply is the same undertaking the compiler-verification work covered elsewhere on this site takes on, giving a domain its own formal semantics and inference rules rather than forcing it into a logic built for something else. The payoff is that quantum correctness properties far richer than mere termination become things you can actually derive.

Prove the logic complete, and let a solver grind through the algebra. A proof system is only trustworthy if it is sound, and only useful if it is complete, so the paper proves both — every derivation is true, and every truth is derivable relative to an oracle for the assertion implications — with the weakest precondition as the linchpin of both arguments. But even a complete logic is punishing to apply by hand, since each step buries the reasoner in matrix manipulations. So the accompanying tool offloads exactly that: it propagates weakest preconditions backward automatically and decides whether one assertion implies another by handing the question to a semidefinite-programming solver, leaving the human to supply only the loop invariants. Discharging the routine, mechanical obligations of a verification task to a numerical solver so the person can focus on the genuinely hard choices is the same division of labour the quantum-error-correction-synthesis work covered elsewhere on this site relies on, casting the grinding part of the problem as constraints a solver dispatches while the designer sets the strategy.

Following the reasoning through the error-correction example

Proving a bit-flip code protects an unknown state

The paper's running example shows why nondeterminism is the natural model, and what a correctness proof must establish.

Step 1 of 5

The code: an unknown error on an unknown qubit

The three-qubit bit-flip code spreads one qubit's state across three, sends them through a noisy channel that may flip at most one of them, then decodes and corrects. Which qubit flipped — or whether any did — is not known, so the program models the channel as a four-way nondeterministic choice: no error, or a flip on the first, second, or third qubit.

The nondeterminism is not a design choice inside the algorithm; it faithfully represents an error the programmer genuinely cannot predict.

Why it works

Defining the program as a set of behaviours makes worst-case correctness expressible. A nondeterministic program has no single behaviour to reason about, which is why classical single-trace logic does not apply → but taking its meaning to be the whole set of super-operators its choices can realize gives a concrete object to quantify over → so correctness can be stated as a guarantee over the worst case in that set, which is exactly what an unknown error demands.
Grounding assertions in Hermitian operators fits the quantum reality. Quantum states are disturbed by measurement and have no true-or-false facts to assert → but an assertion as an observable, satisfied to a degree given by its expectation, captures partial and quantitative satisfaction natively → so the logic can express rich correctness properties, with the identity and zero operators recovering true and false as the extreme cases.
The choice rule turns worst-case reasoning into two ordinary obligations. Proving something for all resolutions of a choice sounds like reasoning about exponentially many executions → but the rule for nondeterministic choice requires only that the same precondition establish the postcondition for each branch → so a four-way error model collapses to four independent, tractable proof goals joined by one rule.
Soundness and relative completeness make the logic trustworthy and sufficient. A proof system that could derive false statements would be worthless, and one that could not derive true ones would be frustrating → but the paper proves, via the weakest precondition, that every derivation is true and every truth is derivable given an assertion oracle → so a failure to find a proof reflects the property, not a hole in the logic.
A solver-backed tool removes the mechanical burden of applying the logic. Even a complete logic is unusable if every step demands pages of matrix algebra by hand → but the assistant propagates weakest preconditions automatically and decides assertion implications with a semidefinite-programming solver → so the user is left to supply only loop invariants, and routine verifications run without human matrix work.

What it costs (trade-offs and scope)

The tool checks only partial correctness. The paper proves logics for both partial and total correctness, but the prototype automates only partial correctness — it can show a program does not produce a wrong answer, but not, by itself, that it terminates. Total-correctness automation is left as future work.
The tool’s soundness is not machine-checked. Unlike Coq- or Isabelle-based provers whose inference rules are verified inside the prover, the Python assistant trusts the paper’s hand proof of soundness. The logic is rigorously proven on paper, but the implementation itself is not formally certified.
It is numerical, not symbolic, so it cannot scale in qubit count. Assertions and operators are concrete numeric matrices, so the tool verifies a program of a specific size, not a family parameterized by an arbitrary number of qubits. A general n-qubit algorithm like Grover can only be checked at fixed sizes, and the matrix backend costs grow exponentially with the qubits.
Performance is exponential and modest in absolute terms. Because the backend manipulates full matrices, verifying a 13-qubit instance of Grover takes about 90 seconds, where a symbolic prover verifies the general algorithm in seconds. The prototype is meant to illustrate the logic, not to be a scalable verifier.
The assertion-implication check has a precision caveat. Deciding whether one assertion implies another uses a semidefinite-programming solver with a small tolerance parameter, so a positive answer is not perfectly certain — though the chance of error is negligible for a small enough tolerance.
The semantics commits to one model of nondeterminism. The paper adopts the lifted model, where all nondeterministic choices are fixed up front, because the alternative relational model cannot be cleanly defined in the quantum setting; this is a principled choice, but it fixes what nondeterminism means in a way that may not match every intended reading.
This is theory plus a prototype, not a production tool. The contribution is the logic — the semantics, the proof rules, and the soundness and completeness theorems — demonstrated on small textbook algorithms. Verifying realistic quantum software at scale is beyond what is shown.

The evaluation

Approaches to reasoning about quantum programs

Property	Deterministic quantum Hoare logic	Termination analysis (nondeterministic)
Handles nondeterministic choice
What it proves
Soundness of the tool	Varies	Not applicable
Symbolic qubit counts	Sometimes	Not applicable
Ease of use	Varies	Not a general tool

Approaches to reasoning about quantum programs. This work is the first with a full correctness logic for nondeterministic quantum programs, proven sound and relatively complete; its NQPV prototype automates partial-correctness proofs in Python with a semidefinite-programming backend, verifying a three-qubit error-correction scheme, the Deutsch algorithm, and a nondeterministic quantum walk (and a 13-qubit Grover instance in about 90 seconds), trading machine-checked soundness and symbolic scale for automation and ease of use.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This paper fills a real hole in quantum program verification: it is the first to give nondeterministic quantum programs a full correctness theory — a denotational semantics as sets of behaviours, partial and total correctness against Hermitian-operator assertions taking the worst case over the nondeterministic choices, and Hoare-style proof rules proven both sound and relatively complete — and it demonstrates the logic on real algorithms including a quantum error-correction scheme. Read it for what it is. The contribution is fundamentally the logic; the accompanying tool is a prototype that automates only partial correctness, is not itself machine-checked (it trusts the paper’s soundness proof), and works numerically rather than symbolically, so it verifies fixed-size instances at exponential cost — 90 seconds for 13-qubit Grover where a symbolic prover does the general case in seconds. Its assertion-implication check carries a small solver-tolerance caveat, and its semantics commits to the lifted model of nondeterminism because the relational one cannot be defined in the quantum setting. The durable value is the theory: a rigorous, complete way to prove nondeterministic quantum programs correct, not just terminating.

Background

Why quantum programs need proofs, not just tests

It is worth seeing why so much effort goes into formally verifying quantum programs rather than simply running and testing them. Testing a classical program means running it on inputs and checking the outputs, but a quantum program resists this at every turn: its state lives in a space that grows exponentially with the number of qubits, so it cannot be inspected directly; measuring it to see what it is doing collapses it and destroys the very superposition that made it quantum; and its outputs are probabilistic, so a single run tells you little. On top of that, the programs that matter most — error-correction schemes, cryptographic primitives, core algorithms — are exactly the ones where a subtle bug is both easy to introduce and catastrophic, and where the hardware they will run on is scarce and noisy, making empirical debugging painful. So the discipline turns to proof: establish once, mathematically, that a program is correct for all inputs and all the ways an unknown error might strike, rather than hoping tests happen to catch a flaw. The same conviction that confidence must come from a proof over all executions rather than from sampling drives the scalable hardware-invariant-learning work covered elsewhere on this site, which likewise argues that for the properties that matter you cannot test your way to certainty. The broader pattern is that as computing moves into regimes we cannot cheaply observe, correctness increasingly has to be proven rather than measured.

If you remember only three things

1. Nondeterministic choice — do this or that, with no rule for which — lets a language express both a specification and its implementations for stepwise refinement, and lets a program model behaviour it does not control, like which error a noisy quantum channel introduced; it had existed in quantum programming for years, but the theory only covered whether such programs terminate, not whether they are correct, and quantum makes verification hard because states are density operators, operations are super-operators with disturbing measurements, and assertions are Hermitian operators satisfied to a numerical degree rather than true or false.
2. This work builds the missing theory: it defines a nondeterministic quantum program's meaning as the set of all behaviours its choices can produce, defines partial and total correctness against operator-valued assertions taking the worst case over those choices (so a program is correct only if it does the right thing for every resolution), and provides Hoare-style proof rules — including a choice rule that reduces worst-case reasoning to proving each branch — that are proven both sound and relatively complete via weakest preconditions; a Python proof assistant, NQPV, automates the routine matrix work using a semidefinite-programming solver.
3. The logic proves a three-qubit error-correction scheme, the Deutsch algorithm, and a nondeterministic quantum walk correct, with the tool verifying a 13-qubit Grover instance in about 90 seconds — but the contribution is fundamentally the theory: the tool automates only partial correctness, is not machine-checked (it trusts the paper's soundness proof), works numerically not symbolically so it handles only fixed-size instances at exponential cost, its assertion check has a solver-tolerance caveat, and its semantics commits to the lifted model of nondeterminism because the relational one cannot be defined in the quantum setting.

Check yourself

Check your understanding

1. Why was verifying nondeterministic quantum programs an open problem?
2. How does the paper define the meaning and correctness of a nondeterministic quantum program?
3. What makes the proof system both trustworthy and usable in practice?
4. Which statement best reflects the limits of this work?

Sources

The paper is “Verification of Nondeterministic Quantum Programs” by Yuan Feng and Yingte Xu, published at ASPLOS 2023, DOI 10.1145/3582016.3582039; the full text used here is the arXiv version, arXiv:2302.07973. The authors are at the University of Technology Sydney, Australia.

This explainer is written from the full 18-page text. Everything above comes from the paper’s own sections: the introduction motivating nondeterministic choice for stepwise refinement and for modelling uncontrolled behaviour, contrasting the relational and lifted models of nondeterminism and noting that the relational model cannot be satisfactorily defined in the quantum setting, and situating the work relative to prior termination analysis; the quantum-computing background on density operators, super-operators, and Hermitian-operator (effect) assertions with expectation-based satisfaction; the syntax of the nondeterministic quantum while-language with its demonic choice construct and the three-qubit bit-flip error-correction scheme written as a four-way nondeterministic program; the denotational semantics defining a program as a set of super-operators with the choice construct as union; the correctness formulas for partial and total correctness taking the infimum over nondeterministic outcomes, the proof systems for both (with the choice, measurement, loop, and union rules) proven sound and relatively complete via weakest (liberal) preconditions and ranking assertions; the case studies of the error-correction scheme, the Deutsch algorithm, and a nondeterministic quantum walk; and the NQPV prototype — a pure-Python proof assistant using ply, numpy, and a cvxpy semidefinite-programming solver that automates partial-correctness proofs, checks the assertion-implication relation by eigenvalue tests or SDP, and is compared against CoqQ, QHLProver, and Qrhl-tool on reliability, expressiveness, automation, usability, and performance (including the 90-second 13-qubit Grover figure).