formalized subsets of x86 assembly exist. Coq can be used as a macro assembler. tools to work with llvm ir exist, x86 can be raised up to llvm ir and proved, kinda bad way tho.