I do not see anything about memory fences. If Jinx does not support them, then it's pretty much useless for verification of synchronization algorithms. I've implemented dozens of advanced synchronization algorithms, and I may say that it's crucial.
Also, if it works on binary level (does not require re-compilation), then it also renders it useless, because on that level you lose information about order of memory accesses, memory fences, atomicity. For example, if you see plain x86 MOV instruction, what is it? non-atomic store? atomic relaxed store? atomic release store?
