The EventB2Java tool generates JML-specified Java implementations for Event-B models. Code generation is based on the definition of some syntactic rules. This paper presents a soundness proof for the translation encoded by those rules. This proof is important as Event-B is typically used to model safety critical systems, and hence we want to increase our trust on that the code generated by EventB2Java is correct. We conduct our proof in Coq. The proof relies on the definition of a state transition semantics for Event-B and JML in Coq. The soundness proof condition states that any transition step in the semantics of JML in Coq is matched by a transition step of the semantic of the Event-B construct from which the JML construct was translated.