test: add executable safety verification envelope

Makefile

@@ -1,4 +1,4 @@
-.PHONY: help install install-dev langgraph-dev test test-unit test-provider openai anthropic nv_build test-integration test-cov test-ci lint lint-fix format format-check clean build docker-build docker-smoke
+.PHONY: help install install-dev langgraph-dev test test-unit test-provider openai anthropic nv_build test-integration test-cov test-ci verify lint lint-fix format format-check clean build docker-build docker-smoke
 
 # Prefer uv if available, else use pip (set when Makefile is parsed)
 UV := $(shell command -v uv 2>/dev/null)
@@ -37,6 +37,7 @@ help:
 	@echo "  make test-provider [openai|anthropic|nv_build] - Run live provider tests"
 	@echo "  make test-integration - Run integration tests only (invokes full graph, may call LLMs)"
 	@echo "  make test-cov       - Run tests with coverage report"
+	@echo "  make verify         - Check deterministic and neural-envelope safety invariants"
 	@echo "  make lint           - Run linters (ruff only)"
 	@echo "  make lint-fix       - Auto-fix lint errors with ruff"
 	@echo "  make format         - Format code with ruff"
@@ -105,6 +106,10 @@ test-cov:
 test-ci:
 	pytest -m "not integration and not provider" --cov=src/skillspector --cov-report=term-missing --cov-report=xml tests/
 
+# Run the fast executable specification and adversarial-oracle property suite.
+verify:
+	pytest tests/verification/
+
 # Run linters (fast: ruff only)
 lint:
 	@echo "Running ruff..."

README.md

@@ -19,6 +19,7 @@ SkillSpector is part of the [NVIDIA Verified Skills pipeline](https://docs.nvidi
 - **[Scan agent skills before installation](https://docs.nvidia.com/skills/scanning-agent-skills)** — Hosted guide: when to scan, how to read a report, and how to gate installs.
 - **[Development guide](docs/DEVELOPMENT.md)** — Architecture, package layout, and how to extend the analyzer pipeline.
 - **[Analysis resource bounds](docs/ANALYSIS_RESOURCE_BOUNDS.md)** — Fail-closed bundle, parser, nested-artifact, ledger, and finding ceilings.
+- **[Verification boundary](docs/VERIFICATION.md)** — Executable safety contracts around deterministic scoring and LLM enrichment.
 - **[Pi extension](docs/PI_EXTENSION.md)** — Install SkillSpector as a Pi tool for scanning skills from inside agent sessions.
 
 ## Features

docs/VERIFICATION.md

@@ -0,0 +1,35 @@
+# Verification boundary
+
+SkillSpector combines deterministic analyzers with optional model inference. Verification
+claims must keep those surfaces separate:
+
+| Stratum | Surface | Contract | Mechanism |
+| --- | --- | --- | --- |
+| S1 | risk scoring and banding | the implementation matches the executable reference model | differential property tests |
+| S2 | deterministic findings crossing the LLM meta-analyzer | arbitrary valid model outcomes cannot remove, invent, or weaken deterministic evidence | adversarial-oracle property tests |
+| S3 | semantic conclusions produced by an LLM | no universal correctness claim | evaluation datasets and provider tests |
+
+Run the fast S1/S2 contract with:
+
+```bash
+make verify
+```
+
+## Phase 1 invariants
+
+- Risk scores are integers in `[0, 100]` and map exhaustively to the documented bands.
+- Diminishing returns apply independently per rule with weights `1`, `0.5`, and `0.25`.
+- Within a rule, findings are ordered by their unweighted score contribution (severity,
+  confidence, and executable provenance together). This makes the score permutation-invariant
+  and monotone: adding non-negative evidence cannot lower the score by taking a larger
+  diminishing-return weight away from stronger evidence.
+- Blocking floors for proven SC8, BH2, and BH3 conditions survive ordinary weighted scoring.
+- Executable-file multiplication is scoped by both source provenance and path.
+- The LLM meta-analyzer may enrich a deterministic finding, but cannot remove it, change its
+  identity or severity, lower its confidence, or create a new deterministic finding.
+
+The reference model in `tests/verification/risk_reference.py` intentionally imports no
+production scoring constants or helpers. A scoring-policy change must update that readable
+specification deliberately. The suite does not claim to verify static detector recall, LLM
+truthfulness, provider availability, or arbitrary malformed data rejected before the typed
+meta-analyzer boundary.

pyproject.toml

@@ -63,6 +63,7 @@ dev = [
     "pytest>=9.0.0",
     "pytest-asyncio>=1.3.0",
     "pytest-cov>=7.0.0",
+    "hypothesis>=6.151.9",
     "ruff>=0.15.0",
     "mypy>=1.19.0",
     "build>=1.4.0",

src/skillspector/nodes/report.py

@@ -453,19 +453,17 @@ def _compute_risk_score(
     to [0, 1]). Findings with confidence <= 0 are skipped entirely — they do not
     contribute to the score but remain in the reported findings list.
 
-    Within each rule_id bucket, findings are processed in severity-descending
-    order so that the highest-severity occurrence always receives the full weight.
+    Within each rule_id bucket, findings are processed by their unweighted score
+    contribution (severity points x confidence x executable multiplier). This gives
+    the strongest evidence the largest diminishing-return weight, makes the score
+    independent of analyzer output order, and ensures adding non-negative evidence
+    cannot lower the score by displacing a stronger occurrence.
 
     Base points per severity: CRITICAL=50, HIGH=25, MEDIUM=10, LOW=5.
     1.3x multiplier applied only to findings from executable script files;
     findings from documentation files (markdown, text, json, yaml, toml)
     are scored at base weight to avoid punishing security documentation.
     """
-    severity_rank = {"CRITICAL": 0, "HIGH": 1, "MEDIUM": 2, "LOW": 3}
-    sorted_findings = sorted(
-        findings,
-        key=lambda f: (f.rule_id or "UNKNOWN", severity_rank.get((f.severity or "LOW").upper(), 4)),
-    )
 
     def component_source_scope(component: Mapping[str, object]) -> str:
         for key in ("source_identity", "source_url", "source_digest"):
@@ -491,6 +489,24 @@ def finding_source_scope(finding: Finding) -> str:
                 cm.get("executable", False)
             )
 
+    def finding_strength(finding: Finding) -> float:
+        confidence = max(0.0, min(1.0, finding.confidence))
+        severity = (finding.severity or "LOW").upper()
+        strength = _SEVERITY_POINTS.get(severity, 5) * confidence
+        if has_executable_scripts and file_executable.get(
+            (finding_source_scope(finding), finding.file), False
+        ):
+            strength *= 1.3
+        return strength
+
+    sorted_findings = sorted(
+        findings,
+        key=lambda f: (
+            f.rule_id or "UNKNOWN",
+            -finding_strength(f),
+        ),
+    )
+
     rule_occurrence_count: dict[str, int] = {}
     score = 0.0
 

tests/nodes/test_report.py

@@ -327,6 +327,17 @@ def test_same_rule_low_before_critical_sorted_correctly(self) -> None:
         # Sorted: CRITICAL first (50*1.0) + LOW second (5*0.5=2.5) = 52.5 -> 52
         assert score == 52
 
+    def test_weak_critical_does_not_lower_score_by_displacing_stronger_high(self) -> None:
+        """Weight allocation follows score strength, not severity alone."""
+        stronger_high = _finding("TM1", "HIGH", confidence=0.1)
+        weak_critical = _finding("TM1", "CRITICAL", confidence=0.01)
+
+        before, _, _ = _compute_risk_score([stronger_high], False)
+        after, _, _ = _compute_risk_score([stronger_high, weak_critical], False)
+
+        assert before == 2
+        assert after == 2
+
     def test_exact_band_boundary_21_is_medium(self) -> None:
         findings = [
             _finding("R1", "MEDIUM", confidence=1.0),

tests/verification/__init__.py

@@ -0,0 +1,4 @@
+# SPDX-FileCopyrightText: Copyright (c) 2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+"""Executable safety specifications for SkillSpector's deterministic envelope."""

tests/verification/risk_reference.py

@@ -0,0 +1,112 @@
+# SPDX-FileCopyrightText: Copyright (c) 2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+"""Small independent reference model for the risk-scoring contract.
+
+This model deliberately does not import production scoring constants or helpers. A
+production change must therefore update this readable specification deliberately,
+rather than making differential tests agree through shared implementation details.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Mapping, Sequence
+from dataclasses import dataclass, field
+
+
+@dataclass(frozen=True)
+class ReferenceFinding:
+    """Only the finding fields that influence the risk score."""
+
+    rule_id: str = "UNKNOWN"
+    severity: str = "LOW"
+    confidence: float = 0.5
+    file: str = "SKILL.md"
+    source_identity: str | None = None
+    source_url: str | None = None
+    source_digest: str | None = None
+    evidence: Mapping[str, object] = field(default_factory=dict)
+
+
+_POINTS = {"CRITICAL": 50, "HIGH": 25, "MEDIUM": 10, "LOW": 5}
+_WEIGHTS = (1.0, 0.5, 0.25)
+_BANDS = ((81, "CRITICAL"), (51, "HIGH"), (21, "MEDIUM"), (0, "LOW"))
+_RECOMMENDATIONS = {
+    "CRITICAL": "DO_NOT_INSTALL",
+    "HIGH": "DO_NOT_INSTALL",
+    "MEDIUM": "CAUTION",
+    "LOW": "SAFE",
+}
+
+
+def _confidence(value: float) -> float:
+    return max(0.0, min(1.0, value))
+
+
+def _source_scope(item: ReferenceFinding | Mapping[str, object]) -> str:
+    for key in ("source_identity", "source_url", "source_digest"):
+        value = getattr(item, key, None) if isinstance(item, ReferenceFinding) else item.get(key)
+        if isinstance(value, str) and value:
+            return f"{key}:{value}"
+    return ""
+
+
+def _score_floor(finding: ReferenceFinding) -> int:
+    if finding.rule_id == "SC8":
+        return 51
+    if finding.severity.upper() != "CRITICAL":
+        return 0
+    if finding.evidence.get("activation_state") != "conditional":
+        return 0
+    if finding.rule_id == "BH2" and finding.evidence.get("proof_status") == "closed":
+        return 51
+    if finding.rule_id == "BH3":
+        return 51
+    return 0
+
+
+def reference_risk_score(
+    findings: Sequence[ReferenceFinding],
+    has_executable_scripts: bool,
+    component_metadata: Sequence[Mapping[str, object]] = (),
+) -> tuple[int, str, str]:
+    """Evaluate the documented scoring contract without production helpers."""
+    executable = {
+        (_source_scope(component), str(component.get("path", ""))): bool(
+            component.get("executable", False)
+        )
+        for component in component_metadata
+    }
+
+    def strength(item: ReferenceFinding) -> float:
+        severity = item.severity.upper() if item.severity else "LOW"
+        value = _POINTS.get(severity, 5) * _confidence(item.confidence)
+        if has_executable_scripts and executable.get((_source_scope(item), item.file), False):
+            value *= 1.3
+        return value
+
+    ordered = sorted(
+        findings,
+        key=lambda item: (item.rule_id or "UNKNOWN", -strength(item)),
+    )
+    occurrences: dict[str, int] = {}
+    score = 0.0
+    floor = 0
+    for finding in ordered:
+        confidence = _confidence(finding.confidence)
+        if confidence <= 0.0:
+            continue
+        floor = max(floor, _score_floor(finding))
+        rule_id = finding.rule_id or "UNKNOWN"
+        index = occurrences.get(rule_id, 0)
+        occurrences[rule_id] = index + 1
+        if index >= len(_WEIGHTS):
+            continue
+        contribution = _POINTS.get(finding.severity.upper(), 5) * _WEIGHTS[index] * confidence
+        if has_executable_scripts and executable.get((_source_scope(finding), finding.file), False):
+            contribution *= 1.3
+        score += contribution
+
+    final = min(100, max(floor, int(score)))
+    band = next(label for threshold, label in _BANDS if final >= threshold)
+    return final, band, _RECOMMENDATIONS[band]