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

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.

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.