A formal and executable specification of the machine using the notation of the Coq proof assistant, with proofs of various properties of the machine and its execution. This is suited for logicians or theoretical computer scientists with knowledge of mechanized mathematics.
This is still work in progress...