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.
