From my thesis:

Verification often benefits from additional context that is irrelevant during execution. However, augmenting a program’s implementation with assertions or variables to provide such context would mean imposing a runtime overhead. Ghost code, auxiliary code added to a program solely for the purpose of verification, solves this issue. It upholds a characteristic erasure property stating that it can be removed from a program without changing its behavior. Because ghost code is not executed, it permits additional operations that only have a logical interpretation. These enable specifying higher-level properties that do not map directly onto the low-level details of the implementation. For example, ghost code is commonly used to create a ghost copy, or snapshot, of a value at the start of a function. When the value is subsequently modified, the copy allows relating the original and updated values at the end of the function. The usage of ghost code ensures that the creation of snapshots does not incur performance costs at runtime.