The problem with memory models is not some much verifying it in a mechanised way, but inventing something suitable at all. Agreed. I'm aware of some work done

The problem with memory models is not some much verifying it in a mechanised way, but inventing something suitable at all. Agreed. I'm aware of some work done a few years ago by people working on weak memory models and extending CompCert with some concurrency primitives: http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/ http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/