AbstractThe Java Card language is a trimmed down dialect of Java aimed at programming smart cards. Java Card specifies its own class file format (the Java Card Converted APplet (CAP) format) that is optimised with respect to the limited space resources of smart cards. This paper deals with the certified development of algorithms necessary for the conversion of ordinary Java class files into the CAP format. More precisely, these algorithms are concerned with constructing and compressing method tables and constant pools. The main contribution of this paper is to specify and prove the correctness of these algorithms using the theorem prover PVS.