We may be able to build on the JML compiler, jmlc, or at least benefit from the results of the collected research efforts of the ESC/Java and JML community [19]. We will strengthen our exisiting links to the ConCert project in CMU and relate our work to the existing work on the Special J proof-carrying native code compiler for Java [20].