Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states.

We present a fully automated framework for verifying the functional correctness of quantum programs with control flow, based on level-synchronized tree automata (LSTA). Our key idea is a choice-sequence semantics that tracks input–output correspondence. We introduce choice-aware inclusion, which enforces this correspondence and enables relational reasoning about program behavior.

We prove a three-test theorem that reduces correctness of RUS protocols to finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implement our approach and identify previously unreported bugs in published RUS constructions.