[nine_k]

I remember there was a theorem that one can find an arbitrary substring in a long enough output of infinite (stationary) random process. I also suppose that a decimal representation of pi may count as one, then your function provably terminates.

But this is of a theoretic interest. In practice the verifier says: "I can't prove that this function will terminate within (some reasonable window), program rejected". And this is what's actually needed: a program that provably has certain properties, where an automatic proof is tractable.

[xigoi]

It is currently not known whether π is a normal number (that is, its representation in any base contains any finite sequence of digits with the same density as in a uniformly random string of digits).