With the possibility to send mobile code between networked machines, strong requirements of security arise, to prevent the execution of malicious code. We are developing a proof-carrying-code (PCC) infrastructure to certify and independently verify that mobile code does not exceed locally available resources (eg. heap space). Starting from a type-based inference of heap consumption for Camelot, we show how this information is used to automatically generate certificates of bounded heap consumption and how this is proven within a VDM-style program logic for JVM bytecode. After giving an overview of the inference and discussing the main features of the logic, I will give a short demonstration of the PCC infrastructure, covering automatic certificate generation from Camelot, and independent verification of the transmitted code and certificate, using the Isabelle/HOL theorem prover.