  We present a simple framework for specifying and proving facts about the
input/output behavior of ELF binary files on the x86-64 architecture. A strong
emphasis has been placed on simplicity at all levels: the specification says
only what it needs to about the target executable, the specification is
performed inside a simple logic (equivalent to first-order Peano Arithmetic),
and the verification language and proof checker are custom-designed to have
only what is necessary to perform efficient general purpose verification. This
forms a part of the Metamath Zero project, to build a minimal verifier that is
capable of verifying its own binary. In this paper, we will present the
specification of the dynamic semantics of x86 machine code, together with
enough information about Linux system calls to perform simple IO.
