Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)

That instinct is right. cuTile would be easier to parse but harder to reason about formally.

We also have a formal memory model and the program semantics are simpler so if anything reasoning about it should be easier.

Oh also good talk at PTC yesterday! I had meant to ask you more about the formal memory model, but the other post talk questions ended up being really interesting too.

Oh really? I can't find anything about the memory model online. I'm not sure what's the best way to do this, but if there's a way for us to get in contact, I'd be interested in adjusting the project so it's developed in the most ergonomic way possible. I'm chatting with a couple of universities and I might issue a research grant for this project to be further fleshed out, so would be keen to hear your insights prior to kicking this off. My email is neel[at]berkeley.edu.