Proof-Carrying Code – jedna z technik matematycznego dowodzenia poprawności programu komputerowego. Koncepcję tę po raz pierwszy w takim sformułowaniu wyraził w 1998 roku George Ciprian Necula.
PCC polega na dołączeniu do skompilowanego programu dowodu spełnialności tzw. warunku weryfikacyjnego tego programu. Weryfikacja tego dowodu może odbyć się po stronie klienta i jej przebieg nie zależy od źródła pochodzenia kodu.
System korzystający z proof-carrying code składa się z: Trusted Computing Base (zaufana baza obliczeniowa), czyli część infrastruktury, której klient ufa. W miarę możliwości powinna zawierać jak najmniej. Zwykle w skład wchodzą: Fizyczny procesor bądź też maszyna wirtualna Generator warunków weryfikacyjnych (Verification Condition Generator) Weryfikator dowodów (w niektórych systemach nie wchodzi on w skład TCB) System operacyjny, biblioteka standardowa, inny wykorzystywany sprzęt itd. Security Policy (polisa bezpieczeństwa), czyli formalny system logiczny złożony z aksjomatów, reguł oraz twierdzenia o bezpieczeństwie mówiącego, że każdy program, którego warunek weryfikacyjny (formuła logiczna powstała przez przeskanowanie kodu binarnego programu, zbudowana według algorytmu, do którego odwoływać się musi twierdzenie) jest spełnialny można uznać za bezpieczny według tej polisy.