...> From what you said in {stuff deleted}, it sounded like you wanted people to manually prove the correctness of the generated assembly, rather than proving the correctness of the high level sounce code. While I could see this being worth while for some programs, it also seems like it would be worth writing those programs in assembly in the first place. No, I want some tool ...