Ghost State

Ghost state is logical state that exists only within a formal proof, not in the running program it reasons about. In program verification, ghost state extends the program's observable state with auxiliary variables, histories, and permissions that have no runtime cost but are essential for stating and proving correctness properties that the physical state alone cannot express.

The technique is most powerful in concurrent verification, where Iris and related frameworks use ghost state to track the logical sequence of operations on shared data structures. A ghost variable might record the order in which threads acquired a lock, or maintain a logical counter that tracks the number of completed operations. Because ghost state is erased before execution, it imposes no performance overhead — yet it enables proofs of properties that would be inexpressible without it.

Ghost state is not arbitrary invention; it must be governed by algebraic composition rules (see Resource Algebra) that ensure local reasoning remains sound when ghost resources are combined or split between threads. The discipline transforms ghost state from an ad-hoc proof trick into a structured reasoning principle.

The existence of ghost state reveals a deep fact about formal reasoning: what is real for the purpose of proof need not be real for the purpose of execution. The program and its proof live in different ontologies, and the art of verification is the construction of a bridge between them.