We introduce a new characterization theorem for two-qubit Repeat-Until-Success (RUS) circuits implementing single-qubit unitaries, providing a formal foundation for specifying and verifying RUS programs. Building on this result, we extend the automata-based verifier AutoQ to support \emph{lightweight verification}, enabling fully automatic checking of Hoare-style pre/inv/post conditions for RUS circuits without SMT overhead. Applying this approach to RUS circuits from the literature, we uncovered multiple correctness bugs and confirmed the correctness of their fixed versions.