[specialgoodness]

This is interesting work but it totally misses the boat when it talks about the current state of the art. They cite a 2014 version of the Goel-Hunt-et al formal x86 model in ACL2, but they fail to talk about its modern version. The modern version (developed at Centaur and then Intel!) is an ACL2 x86 model that is so precise that it can boot Linux and run user-land programs. Let me say that again: it is a formal mathematical model of a processor that is so precise that it can boot Linux and run user-land programs! This is a monumental accomplishment and is not even mentioned in their paper.