Alastair Reid has also done quite a bit with formal verification and specification of the ARM instruction set:

See https://alastairreid.github.io/using-asli/ and cross-references there in