Jinx can help verify mutex implementations themselves, although the example code that ships with the product is a little more advanced (lock-free stack). Some of the underlying technology is described here:
http://s3.amazonaws.com/corensic/whitepapers/DeterministicSh... and here:
http://www.corensic.com/WhyYouNeedJinx/CorensicHasaUniqueTec.... Because it's a hypervisor, it can aid in verifying synchronization primitives that are a mix of userspace and kernel code.
