Intel has recently published a beta executable specification for its ISA: A preview of the future IA documentation | Intel® 64 and IA-32 Architectures Software Developer’s Manual . Although approximations for an ISA specification have existed before (e.g. in ACL2 or SAIL), they were constructed based on the manual in prose form (which had bugs in the past). Having the specification published in an executable language (and hopefully tested!) by the vendor itself is a welcome improvement.
Even better, I just noticed that the interpreter/compiler for the specification language is written in OCaml!