There's a lot of games where certain glitches allow you to actually rewrite the game as you're playing it. Which means that a formal proof would possibly toss you into Turing Complete territory.
For example, a simple shift cipher has one solution that simply and easily produces the expected output. However, a one-time-pad is still incredibly difficult to break to demonstrate that output, even when you may know some key parts of the expected output.
Glitches allow you to write arbitrary data into arbitrary memory positions.
So whilst it is bounded, it is bounded to "any program that can run in less than X time", which as far as I know, is beyond what we can predict within bounded time. The solver may never complete.
Both of these are bounded by existing solutions. We know how many frames, and how many cycles, so you can stop when you get there. Still a very large search space, though.