There has been a steady industry of people retyping the manuals of all the major architectures for use in formal verification. At PLDI last year, there was even a paper where a team used synthesis techniques to automatically generate an instruction spec for x86 by generating tests for processors and using the answers to refine their current guess.

And within ARM, there were lots of people transcribing bits of the ARM manual into various forms: C/C++, LLVM .td files, Verilog, spreadsheets, etc. Apart from all the wasted effort, this also created a verification problem: each transcription had its own set of bugs that now had to be fixed. And it missed a verification opportunity: if everyone used the same master copy then each time one group spots a bug and reports it, the spec gets better for everybody. I talked about this virtuous cycle at S-REPLS last year: https://alastairreid.github.io/papers/srepls4-trustworthy.pd... (S-REPLS is a programming language seminar in SE England.)

This paper might be of interest[0]: Stratified Synthesis: Automatically Learning the x86-64 Instruction Set – PLDI 2016

[0]: https://raw.githubusercontent.com/StanfordPL/stoke/develop/d...