My goal isn't to "prove" the software is correct. My goal is to find as many bugs as I can with the least effort. If I'm able to find all differences in behavior between pgrust and Postgres, sans bugs in the compiler, that's a real win for me

fwiw, I wouldn't say working at the assembly level solves the problem. You now need to make sure that your definition of the assembly behavior is correct