Check reference
Model the decisions the code actually makes
A requirement that says “valid input produces a result” can miss the length, retry and expiry bounds in its implementation. This check points reviewers at those omitted decisions.
The unit is an implementation site
code_predicates_modeled is a specification-stage warning. For active software and integration requirements with FRETish and implementation targets, it gathers load-bearing comparisons from persisted code MC/DC expressions and a conservative source scan. A shared function is one site: any requirement in its family may explain a comparison. An unresolved target does not justify scanning an entire file and attributing every branch to it.
Illustrative example: a document limit
The implementation truncates a document above 5,000 characters. A boolean named document_present says nothing about that boundary. Model the length and include the threshold in the requirement, so 5,000 and 5,001 become distinguishable cases.
variables:
- name: document_length
type: int
direction: input
range: {min: 0, max: 100000}
# Requirement fragment
# when document_length > 5000
# the document_service shall always satisfy document_truncated
The upper domain bound is illustrative. Choose the real input domain, including the invalid region whose handling matters.
Model it or explain its exclusion
Inspect each cited comparison in its function. User-visible limits belong in the model. Incidental structural checks can have a narrow verification.not_modeled entry with a reason, or a co-located proof:domain-exempt: comment. The comment needs a substantive reason. More than three requirement-level exclusions need a tracked [ki:] reference. Review the excluded predicate itself; a blanket explanation cannot establish the omitted behavior.
proof audit --check code_predicates_modeled --verbose
Detection is not equivalence
This is conservative evidence about missing model detail, not proof that the formalization matches all code paths. A passing scan does not demonstrate that a typed variable is measured correctly at runtime. Keep source bindings, executed boundary tests and the justification for exclusions with the requirement. Warning severity is separate from audit's configured failure policy.
Follow the evidence
Review the first named comparison together with the requirement that owns its outcome.
Review one omitted code decision. Bring the named comparison and its requirement so we can assess whether the bound belongs in the model or needs an explicit exclusion.