I haven't read it (yet), but seems interesting... Formal Verification of Application and System Programs Based on a Validated x86 ISA Model: http://www.cs.utexas.edu/~shigoel/x86isaInfo/Shilpi-Goel-Dissertation.pdf