Check reference

Check the system requirement record

Before reviewing whether a system requirement is right, its record needs enough structure to state what it promises and where it came from. l1_system_complete checks that minimum shape.

What the check observes

For active system requirements, the current predicate checks for a satisfies entry and a nonempty description. If the record explicitly selects the FRETish strategy, it also requires a nonempty FRETish field. Retired, superseded, and rejected records are excluded. This is a field-presence check; it does not establish that the parent relationship is semantically correct or that the formula captures the description.

Example: a formalization strategy without a formula

Illustrative case. A requirement has a system description and a parent but declares fretish formalization while leaving the formula blank. The record claims a modeling approach that has not yet been supplied.

# Incomplete record excerpt
id: SYS-REQ-042
description: "Reject a transfer when the account balance is insufficient."
formalization_strategy: fretish
fretish: ""
traces:
  satisfies: [STK-REQ-007]

Resolve the finding

Read the missing-field details and identify the intended system behavior and stakeholder source.
Complete the description and legitimate parent relationship. Where FRETish is the selected strategy, model the actual conditions and response, including relevant domain bounds.
If a different strategy is justified, choose it through project policy. Do not downgrade the strategy solely to avoid creating the required formalization.

Run and interpret

proof audit --check l1_system_complete --verbose

This is a specification-stage error check. A project with no system requirements reports that there are none to inspect; the result is not evidence that a system specification is complete. The workflow also respects explicit level skips.

The check does not judge ambiguity, correctness, decomposition quality, implementation, or test execution. In particular, a present satisfies entry is weaker than a verified relationship to the intended stakeholder requirement. Review that relationship and use the applicable trace and consistency checks.

Continue from here

Inspect upward trace presence. Review whether the requirement is right.

Bring a system requirement whose record is complete but whose meaning remains hard to review. Bring a change to Proof.