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/