General methods of verification for programs defining infinite computataions rely on measuring progress or convergence of finite computations towards satisfying the specification. Traditionally, progress is measured using well-founded orderings, but this often involves syntactic transformations. Our main result is that program verification can take place by direct measurement of convergence for programs that are analytic ($\sum^{1}{1}$) sets and specifications that are coanalytic ($\prod^{1}{1}$) sets. We use orderings that are not well-founded, but that ensure well-foundedness of limits of finite trees. Our results can also be seen as a new approach to parts of descriptive set theory. In fact, Souslin's Theorem-that every set in $\sum^{1}{1} \cap \prod^{1}{1}$ is Borel-is a simple corollary of our main result.