携带证明的代码(Proof-Carrying Code，PCC)最早由Necula提出，其定义是可执行代码携带上关于自身安全性的形式证明。代码消费方不需要信任PCC代码的生产方，即可执行代码与安全性证明不再属于整个系统安全性的信任计算基础(Trusted Computing Base，TCB)。随后Appel与Felty提出了基础性携带证明的代码(FoundationalProof-Carrying Code，FPCC)的概念。 FPCC的基本思想是将PCC代码与复杂的推理系统都形式化在一个底层的基础逻辑(Foundational Logic)中，于是推理系统的可靠性就可以用基础逻辑保证，复杂的推理系统可以被排除出TCB，其TCB仅包括安全策略、机器模型、基础逻辑以及基础逻辑的证明检查器。 随后的各种FPCC实现采用了不同的推理系统来构造代码的安全性证明。例如采用类型系统(如LTFAL，TALT)或者采用逻辑系统(如SCAP)，还有一些FPCC系统同时采用了类型与逻辑的混合系统作为推理系统(如OCAP,Open Verifier)。