Proof-carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code.
The original publication on proof-carrying code in 1996[1] used packet filters as an example: a user-mode application hands a function written in machine code to the kernel that determines whether or not an application is interested in processing a particular network packet.
Traditional approaches to this problem include interpreting a domain-specific language for packet filtering, inserting checks on each memory access (software fault isolation), and writing the filter in a high-level language which is compiled by the kernel before it is run.
The steps of this proof are recorded and attached to the machine code which is given to the kernel program loader.
The program loader can then rapidly validate the proof, allowing it to thereafter run the machine code without any additional checks.