The inaugural paper in this category describes using Coq to create a formalised subset of the x86 architecture.