alt Hacker NewsYou can do the process in stages. Do the first decompilation mechanically (no LLM), use a SMT solver to show it builds to an equivalent binary to the original, and then use LLM to clean up the code into something idiomatic with the benefit of a correct binary built with the new toolchain. This helps when you want to port across languages or toolchains, and helps protect against toolchain bugs.
In my project I've been practicing a similar loop as you describe: an agent writes code, SMT solver checks against a spec. A few things I observed:
1. Solver is great at the bugs tests miss (overflow, off-by-one, empty inputs...), its output can be used by the agent to fix it.
2. Solver struggles where you'd assume: loops, non-linear arithmetic and pointer aliasing blow up solve time, floating point is painful.
So your step 2 would cover some of it well, but since the game code is a lot of floating point, SMT would probably have a hard time (get stuck/timeout).