Using the Isabelle theorem prover [10] we have developed a programming logic for Java bytecode, and demonstrated that it can be used to prove properties of simple bytecode programs involving loops. Our motivation for this was to produce a method by which Java Just-In-Time (JIT) compilers could be assisted to produce more efficient code. This paper discusses the issues involved in the development of the programming logic as it stands, and suggests possible extensions to it. We also describe our experiences of the difficulties inherent in carrying out proof at the level of bytecode instructions, along with the benefits and disadvantages of using a mechanized proof tool.