We have written a formal specification of the iVM abstract machine, aimed at mathematically minded readers. The motivation for this description is that we assume that mathematical knowledge will remain understandable to future readers longer than technological knowledge.
The specification has been formalized and mechanically checked using the Coq Proof Assistant. The mathematical machine description has been extracted from a Coq formalization using the tool coqdoc, which makes it possible to mix formalized mathematics with explanations in natural language. Details in the Coq code that are not necessary to understand the specification have been left out.