Klient infrastruktury PCC musi albo przestudiować dowód twierdzenia o bezpieczeństwie albo mu zaufać – każdy błąd w dowodzie jest potencjalną luką w bezpieczeństwie PCC.
Gwarancje bezpieczeństwa Podstawowe trudności w przemysłowym sformułowaniu PCC polegają na tym, że formalizacje polis bezpieczeństwa są zwykle bardzo trudne lub dyskusyjne. Dość dobrze wyraża się polisy gwarantujące bezpieczeństwo typów czy poprawne kontraktowanie, ale wiele innych ciekawych formalizmów (m.in. Non-Interference) ma charakter bardziej teoretyczny, możliwy do zaaplikowania do algebraicznych modeli procesów, a nie ich konkretnych instancji wyrażonych w językach niskiego poziomu.
Ponadto definicja algorytmu generatora warunków weryfikacyjnych i dowód twierdzenia o bezpieczeństwie musi być powtórzony dla każdej pary polisa bezpieczeństwa – kod maszynowy. Dowody takie są trudne, żmudne i niemożliwe do automatycznej weryfikacji.