Code signal obligations reviewed

The check is code_signal_obligations_reviewed. It is opt-in at verify. Enable it when you are ready to review code-derived obligations:

proof config set project.checks.code_signal_obligations_reviewed.enabled true

It consumes two bounded sources. Live built-in scanner signals from Go, Rust, and Zig artifacts linked from requirements. Cached external-provider reports under the configured signals directory when that provider is enabled, including auto-detected Slither. A disabled provider is ignored even when a cache file exists. Solidity, JavaScript, and TypeScript participate through those normalized reports, not through a second native scanner.

These are not bug verdicts. A goroutine, an http.Get without a context, a map-range, a filesystem call: the hop forces the owning requirement family to specify, test, suppress, or defer that risk. Inferred tags stay visible for catalog navigation. Tags do not silently create required obligations. Only an explicit obligations: list on a pack, a custom pack, or project.signals.mappings creates a gap.

func FetchPolicy(url string) ([]byte, error) {
    resp, err := http.Get(url) // no context, no timeout
    if err != nil {
        return nil, err
    }
    defer resp.Body.Close()
    return io.ReadAll(resp.Body)
}
# SYS-REQ-014 implemented_by: FetchPolicy
# obligation_checklist does not list external_call_timeout_bounded
# pack maps http.request_without_cancellation -> that class
# warn: FetchPolicy / external_call_timeout_bounded untriaged
# silent scanner: the SARIF exists. the owner never listed the class

A direct code-signal finding closes only when the related requirement family has all three pieces: the class on obligation_checklist, an implemented_by trace to the signaled artifact, and verification evidence (verified_by, or informal verification with non-empty evidence). Adding the class to the checklist alone does not close it. That only declares decomposition work.

A draft class id that does not resolve stays on code signal unbindable. A listed class with no signal stays on obligation enforcement backed. A tag-matched class that was never listed stays on obligation baseline. A covering SYS-REQ stays on obligation completeness. Four inventories of existing classes stay on catalog completeness.

Inspect the matrix before trusting a green summary. Grouped hits (same provider, rule, artifact, obligation set) are one finding, not one warning per tool location. An artifact with no owner is named until an implemented_by trace exists. A KnownIssue-backed row stays a warning, counted separately, never folded into covered. A valid deferral is tracked debt, still a warning, never untriaged and never a silent drop.

proof signals matrix --format markdown
proof signals findings list --obligation external_call_timeout_bounded
proof catalog show external_call_timeout_bounded --plain-english
proof req edit SYS-REQ-014 --add-obligation external_call_timeout_bounded
proof audit --check code_signal_obligations_reviewed

Close it on the existing approved owner when the artifact already has one. Do not mint a draft requirement just to carry the class. A fresh draft trips changed_requirements_reviewed, and agents cannot approve. Suppress only when the shape is outside that requirement's contract, with a reason. Defer only with a long reason and a tracking ref.

The teaching graph is still one HTTP get whose SARIF is present and whose owner never listed the timeout class. Close it on SYS-REQ-014. Do not treat a Jama note as this hop. Do not treat a scanner file as a covering requirement.

proof audit --check code_signal_obligations_reviewed --verbose
proof signals matrix --format json
proof workflow check --stage verify --verbose

The draft-class hop stays on code signal unbindable. The silent-no-op hop stays on obligation enforcement backed. The silent-omission hop stays on obligation baseline. The covering-child hop stays on obligation completeness. The presence hop stays on obligation evidence complete. The four-invariant hop stays on catalog completeness. Jama still authors. Proof vs Jama.

Opt-in. Disabled by default. Enable it, or the hop never runs. No signals is a silent pass. Severity of an untriaged finding is warning, not fail. Promote once the corpus is clean. The hop does not claim the detector found every bug in the class. It claims a fresh, normalized signal is strong enough to require a review. Built-in live claims are syntax-bounded: direct Go, Rust, and Zig shapes, configured selectors, and the documented Rust span-pair detectors. Broader taint and other languages ride cached provider evidence that must be fresh. A missing, unavailable, or changed source_hash is stale-cache guidance, never a silent trust. Tags do not create obligations. Checklist-only does not close a direct gap. A KnownIssue-backed row stays a warning. A valid deferral stays a warning. The hop does not write the requirement. It does not bind verified_by for you. It does not prove the Go. An explicit opt-out reports skip, not pass. We have not scored this floor against a frozen Jama pack, a CodeSignal interview, or a frozen OpenGrep corpus. The loss is named, not scored.

The draft-class hop stays on code signal unbindable. The silent-no-op hop stays on obligation enforcement backed. The engagement stays on software correctness audit. Jama still authors.

What is code signal obligations reviewed? Same question. Same URL.

Is this CodeSignal? No. Ads code signal is that interview product. A hosted kata is not this cell.

Is this code signal unbindable? No. That hop is whether proposes_class still names a class that does not exist. This hop is whether an existing class implied by the signal is owned. See code signal unbindable.

Is this obligation enforcement backed? No. That hop is whether a listed class has a signal or any evidence. This hop is the other direction: a signal whose class was never listed. See obligation enforcement backed.

Is this obligation baseline? No. That hop is whether a tag-matched class was listed, suppressed, or delegated. Tags here do not create the gap. See obligation baseline.

Does adding the class to obligation_checklist close it? No. The family still needs an implemented_by trace and verification evidence.

Does a disabled check fail? No. The hop is opt-in. Disabled is skip, never pass.

Does a green hop prove the Go? No. The hop observes that a fresh signal is owned, suppressed, or deferred. It does not prove the function is correct.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.