In het kader van deductieve programmaverificatie maakt ghostcode deel uit van het programma dat wordt toegevoegd ter specificatie. Ghost-code mag de reguliere code niet verstoren, in die zin dat deze kan worden gewist zonder waarneembaar verschil in de uitkomst van het programma.
