Writing a Fuzzer for NES Games
pseudorandom.resistant.tech
pseudorandom.resistant.tech
Presumably that would first require a disassembly of the game, with a proven compilation process back to the original ROM (something like what CompCert does[0]) and then, after enumerating all the possible glitches, building some sort of state machine that defines how the character can progress through each level.
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.