Hun antar at oppdateringen kom fra leverandøren og var ikke tuklet med i transitt, snarere enn fra en angriper prøver å lure henne til å installere en falsk lapp som skulle egentlig åpne sikkerhetshull.

Hun er forutsatt at leverandøren testet oppdateringen grundig. Leverandører er ofte under sterkt press til å utstede patcher raskt og noen ganger teste dem bare mot en bestemt angrep. Sårbarheten kan være dypere, men og andre angrep kan lykkes. Når noen har gitt ut en utnyttelse av en leverandørs operativsystem kode, ga selgeren korrigere en lapp i 24 timer. Dessverre åpnet lappen en andre hull, en som var langt enklere å utnytte. Den neste oppdateringen (gitt ut 48 timer senere) fast begge problemer riktig.

Hun er forutsatt at leverandørens testmiljø tilsvarer miljø henne. Ellers kan oppdateringen ikke fungerer som forventet. Som et eksempel, en leverandørens lapp gang tilbakestille eierskap av kjørbare filer til brukeren root. På enkelte installasjoner, vedlikehold kreves at disse kjørbare være eid av brukeren bin. Leverandørens lapp måtte gjerast og løst for lokal konfigurasjon. Denne antakelsen omfatter også mulige konflikter mellom ulike lapper, samt patcher som er i konflikt med hverandre (for eksempel lapper fra forskjellige leverandører av programvare som systemet bruker).

Hun antar at oppdateringen er installert riktig. Noen flekker er enkle å installere, fordi de er bare kjørbare filer. Andre er komplisert, krever systemansvarlig konfigurere nettverket orientert egenskaper, legge til en bruker, endre innholdet i et register, gir rett til noen sett med brukere, og deretter starte systemet. En feil i noen av disse trinnene kan hindre lappen fra fikse problemene, kan som en inkonsekvens mellom miljøer der oppdateringen ble utviklet og hvor plasteret er brukt. Videre kan lappen hevder å kreve spesielle privilegier, da i realiteten privilegiene er unødvendige og faktisk farlig

Den formelle verifisering av S er correctthat er, har beviset ingen feil. Fordi formell bekreftelse er avhengig av automatiserte teorem provers samt menneskelig analyse må teoremet provers programmeres riktig.

Forutsetningene gjort i den formelle bekreftelsen av S er korrekte, spesielt de forutsetningene holder i miljøet der programmet er å bli henrettet. Disse forutsetningene er vanligvis fôret til teoremet provers samt programmet S. En implisitt aspekt av denne antakelsen er at den versjonen av O i miljøet som programmet skal kjøres er den samme som den versjonen av O brukes til å verifisere S.

Programmet vil bli forvandlet til en kjørbar hvis handlinger er tilsvarende de som indikeres av kildekoden, med andre ord kompilatoren, linker, lader, og alle bibliotekene er riktige. Et eksperiment med en versjon av UNIX-operativsystemet vist hvor ødeleggende en rigget kompilator kunne være, og angripere har erstattet biblioteker med andre som utførte tilleggsfunksjoner, og dermed øker sikkerhetsrisikoen.

Maskinvaren vil kjøre programmet som forutsatt. Et program som er avhengig av flytende punktet beregninger ville gi uriktige resultater på enkelte datamaskinen CPU chips, uavhengig av formell verifikasjon av programmet på grunn av en feil i disse sjetonger. Tilsvarende, et program som er avhengig av innspill fra maskinvaren forutsetter at bestemte vilkår gi dem innganger