1. A method comprising: generating a boot code for a peripheral device from a program written in a high-level programming language; gathering information while generating the boot code; and generating a certificate from the information gathered while generating the boot code, wherein the certificate describes operation of the boot code, and wherein the certificate includes an annotation defining a proof of security and safety for both (i) one or more blocks of code generated from a low-level programming language different from the high-level programming language and (ii) one or more corresponding blocks of the boot code resulting from translation of the one or more blocks of the code of the low-level programming language into the high-level programming language.