While I completely agree with 3uru, where it can get stuck is if your system contains a pseudorandom generator or some other cryptographic shenanigans. These are programs deliberately made difficult to analyze and reason about.

I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).