An instruction set architecture is an abstraction, a common interface layer between the software and the micro-architecture. The existence of this clearly delineated interface is becoming increasingly important as hardware designers find new and unusual ways to break the laws of time and space with out-of-order execution, cache coherency (or lack thereof), and of course concurrent processing at every level.
The question is, what is the appropriate setting for defining the ISA itself such that we can specify familiar operations like ADD and LOAD and STORE and also unfamiliar ones like non-temporal stores, locking instructions, and hardware interrupts (which don't even come with an instruction to step!).
What I think is the "classical" answer is to have a state machine where the state is a tuple containing the values of the registers (including the PC) and the state of memory, and the state transitions include things like "if the instruction at the PC is EAX = EAX + 1 then the new state is the same as the old state but with EAX increased by 1 and the PC incremented by the size of the instruction". But while this works well for simple examples, it's not obvious how to apply it to, say, the Intel x86 architecture, which has instructions like the aforementioned non-temporal store that don't simply write to the state's memory in a way that would be reflected by a later LOAD.
Furthermore, it would also be useful in many cases to be able to simplify the ISA in two ways. If a program doesn't use a bunch of old or complicated instructions then it may want to promise that it doesn't execute those commands, and so it can be correct against a reduced ISA where the instructions that lead to the old instructions are instead considered "bad states" to be avoided, so that the state transitions leading out of these states don't matter. Second, if certain parts of the state are set in a complicated way that doesn't matter to the program (e.g. random instructions changing the flags), it may want to underapproximate this behavior by using nondeterminism to say "this is set to something but I don't know what and I should be prepared for any result".
In fact even without ISA refinements both these effects already exist in the complete spec - there are bad states in the form of "reserved for future use" instructions (plus faulting instructions if you don't consider that legitimate control flow), and nondeterminism in the form of undefined values and explicit concurrency.
What are the common approaches to dealing with all this mathematically? How can we formalize industrial-grade ISAs without lying (but possibly saying less than the whole truth)? References are welcome.