This paper introduces a formal verification of

m

Java compiler targeting Micro-Dalvik virtual machine(VM) where

m

Java is an object-oriented language similar to Java

and Micro-Dalvik is a Dalvik-like VM of the register-based architecture.The operational semantics of

m

Java and Micro-Dalvik VM are defined.The compiler operates in two stages.First it replaces the names of local variables by their corresponding indice

s and hence translates

m

Java into an intermediate language.Then it generates the Micro-Dalvik VM instructions.After defining the operational semantics of the intermediate language

the correctness of the two stages are formulated in terms of the preservation of the semantics and is proved respectively.The whole formalization is machine-checked in the theorem proof assistant Isabelle/HOL.The

m

Java language and Micro-Dalvik VM are more abstract than the comparable Java and the Dalvik VM

respectively

which is a result of a compromise between the the realism of the language and the clarity of the formalization.However

m

Java language and Micro-Dalvik VM exhibit core features of an object-oriented programming language and a register-based architecture

respectively

and thus in this sense

this verified compiler is non-trivial.