Check reference
Resolve variables with no requirement to explain them
A variable declaration should support a real behavioral obligation. variable_orphans_clean exposes both unused declarations and requirement names without declarations.
Read the direction of the mismatch
A declared-unused finding can reveal a forgotten requirement, a rename leftover or speculative modeling. An undeclared-used finding can indicate a typo or a requirement assigned to the wrong component. The default check severity is error. For requirements with FRETish, parsed formula use is the usage reference, so a stale metadata list should not keep a dead variable alive. Non-FRETish requirements use their authored list.
Illustrative example: a stranded cancellation signal
A component declares cancel_requested, but its active requirements only describe starting and completing jobs. Decide whether cancellation is supported behavior before editing the variable file.
If cancellation is supported:
write the missing obligation and its expected state transition.
If cancellation was removed:
remove the obsolete declaration after checking consumers.
If the signal is proof bookkeeping:
record a truthful auxiliary reason.
The first option should describe real intended behavior. Creating a token requirement merely to consume the name would hide the modeling gap.
Inspect consumers at the component boundary
Use the variable diagnostic to see declaration location, direction and consuming requirements. Correct spelling and ownership before adding a duplicate declaration. An auxiliary exemption needs proof_auxiliary: true and a substantive proof_auxiliary_reason; it is appropriate for solver bookkeeping, not unfinished product requirements.
proof var diagnose worker
proof gaps specs/system --check orphans
proof audit --check variable_orphans_clean --verbose
An orphan-free inventory is still only an inventory
Every variable can have a consumer while the model omits important inputs or uses the wrong bounds. Follow up with domain, gap and code-predicate checks. Deleting an unused declaration does not establish that the real system lacks the corresponding behavior. Retain the product decision and review impact on any code or tests that still refer to it.
Follow the evidence
For each orphan, choose a real missing requirement, a documented helper role, or deletion.
Review one orphaned variable. Bring its declaration and intended consumers so we can distinguish missing behavior from obsolete names or genuine proof bookkeeping.