Deduktiivisen ohjelman todentamisen yhteydessä haamukoodi on osa ohjelmaa, joka lisätään määrittelyä varten. Haamukoodi ei saa häiritä tavallista koodia siinä mielessä, että se voidaan pyyhkiä ilman havaittavia eroja ohjelman tuloksessa.
