Ghost Variables
Track proof-only facts beside runtime state, then erase them from the compiled program. Use ghost variables to express history, ownership, and invariants that normal fields cannot capture cleanly.
Ghost Blocks
Update proof-only state beside runtime changes. Keep invariants synchronized without adding deployed code.
Ghost Functions
Name reusable proof logic without shipping it. Keep contracts readable and share verifier-only vocabulary.
Ghost Modules
Package proof state behind module boundaries. Expose clean contracts while hiding verifier machinery.
Ghost Patterns
Use mirrors, conservation models, and history tracking to turn messy behavior into stable invariants.