Ah, interesting. I went with Ghidra p-code which seems ok but what I didn't really appreciate going in was how much of the platform API surface you have to describe before you can prove pretty much anything at all.