Formal specifications aren't only useful for proving properties of programs. They can also be useful for providing definitive answers to questions about example program behavior which is useful for regular programmers.
For example the Herd tool kit can take small concurrent programs with some constraints and a memory model and then answer whether any executions are possible.
For example the Herd tool kit can take small concurrent programs with some constraints and a memory model and then answer whether any executions are possible.
http://diy.inria.fr/doc/herd.html
Alternately there is the online tool for the same purpose for ARMv8:
https://www.cl.cam.ac.uk/~sf502/regressions/rmem/