In case someone else is interested in this kind of work, there's an interesting line of research in certified programs that's similar to this. Basically, you specify the semantics of some language in Coq. Then, write a program in the desired language. This allows us to analyze the program in Coq and prove certain properties about it. Essentially, it's a process to develop certified programs by using the process:

language -> Coq -> prove properties

As another example of this, Sandrine Blazy and Xavier Leroy have a paper that formalize a subset of C in Coq:

http://pauillac.inria.fr/~xleroy/publi/Clight.pdf

There's also some discussion on StackOverflow about the definition of what a certified program is:

https://stackoverflow.com/questions/21320138/definition-of-a...

In any case, formalizing a subset of the x86 architecture in Coq means that we can prove properties about a program written in assembler using Coq, which is both interesting and impressive.