Source: wikibot/proof-carrying-code

= Proof-carrying code
{wiki=Proof-carrying_code}

Proof-carrying code (PCC) is a formal method used in computer science, particularly in the field of software verification and security. The concept involves attaching a formal proof to a piece of code which guarantees that the code adheres to specific safety and security properties. Here’s a high-level overview of how it works: \#\#\# Key Concepts: 1. **Code and Proof**: When a developer writes code, they also generate a proof that the code satisfies certain properties.