feat: add correctness traversal and verification-sufficiency passes

CHANGELOG.md

@@ -4,9 +4,11 @@ summary: Chronological history of repository and skill changes.
 
 # Changelog
 
-## 2026-07-28 — Added consumer/impact-traversal evidence and required passing validation and current-head lens evidence for a clean review verdict
+## 2026-07-28 — Added correctness traversal and verification-sufficiency passes, consumer/impact-traversal evidence, and required passing validation and current-head lens evidence for a clean review verdict
 
+- feat: add correctness traversal and verification-sufficiency passes
 - feat: add consumer/impact-traversal evidence to the shared review contract
+  (`8e4fdbdaad8f70751d45f8c2ca87e88288f8ba5b`)
 - feat: require passing validation and current-head lens evidence for a clean
   review verdict (`b1e51979628652e4ef60adad44089bf54f4551e7`)
 

review-suite/CONTRACT.md

@@ -206,6 +206,39 @@ the same way this contract family already judges any other lens-specific finding
 (a duplicated-policy or behavior-bug miss is likewise never something this
 schema-and-structure validator can detect on its own).
 
+### Verification-sufficiency evidence
+
+A `correctness` or `aggregate` result may record
+`verification_sufficiency_evidence`: one entry per claimed validation command or
+test that touches a materially risky change, each naming the
+`claimed_test_or_command`, whether it `exercises_material_risk` (`yes`, `no`, or
+`not_applicable`), and `reasoning` describing what specific triggering condition
+was or was not exercised.
+
+This makes a reviewer's verification-sufficiency judgment machine-checkable:
+asking whether a claimed test would actually fail for the specific triggering
+condition a change addresses, not merely whether it passes. It closes a baseline
+verification-sufficiency miss, where the added test exercised an already-safe
+branch (an owned entry) rather than the actual risk (an owner-absent
+interleaving), so the passing test proved nothing about the risk it was meant to
+cover.
+
+Given a supplied entry:
+
+- only `correctness` or `aggregate` results may include this evidence;
+- an entry exists only because a claimed test or command touches a materially
+  risky change, so `exercises_material_risk: "no"` is itself the gating fact — a
+  `clean` verdict must not pair with such an entry, because that would silently
+  hide exactly the gap this evidence exists to surface; and
+- `exercises_material_risk: "yes"` or `"not_applicable"` may pair with `clean`
+  when no other gating finding remains.
+
+As with consumer/impact evidence, this validator cannot itself decide which
+claimed tests required an entry — that judgment belongs to the lens performing
+the pass. An omitted `verification_sufficiency_evidence` array remains
+schema-valid; completeness of a given pass is judged by forward-testing the
+lens's actual output against a fixture's expected result.
+
 ## Simplification proposal dispositions
 
 When an orchestrator asks correctness to assess a validated simplification

review-suite/contracts/review-result.schema.json

@@ -13,7 +13,7 @@
     "blocking_reasons"
   ],
   "properties": {
-    "schema_version": {"const": "1.2"},
+    "schema_version": {"const": "1.3"},
     "lens": {
       "enum": [
         "correctness",
@@ -145,6 +145,23 @@
         }
       }
     },
+    "verification_sufficiency_evidence": {
+      "type": "array",
+      "items": {
+        "type": "object",
+        "additionalProperties": false,
+        "required": [
+          "claimed_test_or_command",
+          "exercises_material_risk",
+          "reasoning"
+        ],
+        "properties": {
+          "claimed_test_or_command": {"type": "string", "minLength": 1},
+          "exercises_material_risk": {"enum": ["yes", "no", "not_applicable"]},
+          "reasoning": {"type": "string", "minLength": 1}
+        }
+      }
+    },
     "proposal_dispositions": {
       "type": "array",
       "items": {

review-suite/fixtures/auth-regression/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "correctness",
   "candidate": {
     "head_sha": "8181818181818181818181818181818181818181",

review-suite/fixtures/behavior-bug/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "correctness",
   "candidate": {
     "head_sha": "1111111111111111111111111111111111111111",

review-suite/fixtures/clean-change/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "aggregate",
   "candidate": {
     "head_sha": "5555555555555555555555555555555555555555",

review-suite/fixtures/code-simplicity-clean/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "code_simplicity",
   "candidate": {
     "head_sha": "8c8c8c8c8c8c8c8c8c8c8c8c8c8c8c8c8c8c8c8c",

review-suite/fixtures/complexity-relocating-wrapper/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "code_simplicity",
   "candidate": {
     "head_sha": "8989898989898989898989898989898989898989",

review-suite/fixtures/consumer-impact-traversal/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "aggregate",
   "candidate": {
     "head_sha": "6262626262626262626262626262626262626262",

review-suite/fixtures/duplicated-policy/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "code_simplicity",
   "candidate": {
     "head_sha": "2222222222222222222222222222222222222222",

review-suite/fixtures/explicit-tests-preserved/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "code_simplicity",
   "candidate": {
     "head_sha": "8b8b8b8b8b8b8b8b8b8b8b8b8b8b8b8b8b8b8b8b",

review-suite/fixtures/imagined-machinery/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "solution_simplicity",
   "candidate": {
     "head_sha": "3333333333333333333333333333333333333333",

review-suite/fixtures/manifest.json

@@ -15,6 +15,7 @@
   {"name": "missing-simplification-requirements", "packet_valid": true},
   {"name": "clean-change", "packet_valid": true},
   {"name": "consumer-impact-traversal", "packet_valid": true},
+  {"name": "verification-sufficiency-guard", "packet_valid": true},
   {"name": "missing-evidence", "packet_valid": false},
   {"name": "unrelated-base-drift", "packet_valid": true}
 ]

review-suite/fixtures/missing-evidence/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "aggregate",
   "candidate": {
     "head_sha": "6666666666666666666666666666666666666666",

review-suite/fixtures/missing-simplification-requirements/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "solution_simplicity",
   "candidate": {
     "head_sha": "8686868686868686868686868686868686868686",

review-suite/fixtures/missing-test/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "correctness",
   "candidate": {
     "head_sha": "8282828282828282828282828282828282828282",

review-suite/fixtures/multi-pass-control-flow/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "code_simplicity",
   "candidate": {
     "head_sha": "8888888888888888888888888888888888888888",

review-suite/fixtures/necessary-complexity/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "solution_simplicity",
   "candidate": {
     "head_sha": "4444444444444444444444444444444444444444",

review-suite/fixtures/repository-convention-clean/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "correctness",
   "candidate": {
     "head_sha": "8383838383838383838383838383838383838383",

review-suite/fixtures/shared-test-setup/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "code_simplicity",
   "candidate": {
     "head_sha": "8a8a8a8a8a8a8a8a8a8a8a8a8a8a8a8a8a8a8a8a",

review-suite/fixtures/speculative-backfill/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "solution_simplicity",
   "candidate": {
     "head_sha": "8585858585858585858585858585858585858585",

review-suite/fixtures/unrelated-base-drift/expected.json

@@ -1,5 +1,5 @@
 {
-  "schema_version": "1.2",
+  "schema_version": "1.3",
   "lens": "aggregate",
   "candidate": {
     "head_sha": "7777777777777777777777777777777777777777",

review-suite/fixtures/verification-sufficiency-guard/expected.json

@@ -0,0 +1,19 @@
+{
+  "schema_version": "1.3",
+  "lens": "correctness",
+  "candidate": {
+    "head_sha": "7373737373737373737373737373737373737373",
+    "comparison_base_sha": "3737373737373737373737373737373737373737"
+  },
+  "verdict": "clean",
+  "findings": [],
+  "blocking_reasons": [],
+  "verification_sufficiency_evidence": [
+    {
+      "claimed_test_or_command": "tests/test_claims.py::test_release_denied_when_owner_absent_and_not_expired",
+      "exercises_material_risk": "yes",
+      "reasoning": "Sets snapshot owners to {} (owner absent) and constructs the claim with expired=False, exactly the triggering condition the new `owner is None and not claim.is_expired()` guard clause addresses, and asserts release is still denied."
+    }
+  ],
+  "next_action": "No material review action is required."
+}

review-suite/fixtures/verification-sufficiency-guard/packet.json

@@ -0,0 +1,28 @@
+{
+  "schema_version": "1.0",
+  "repository": {"identity": "example/coordinator", "base_branch": "main"},
+  "candidate": {
+    "head_sha": "7373737373737373737373737373737373737373",
+    "comparison_base_sha": "3737373737373737373737373737373737373737",
+    "diff": {
+      "format": "unified_diff",
+      "complete": true,
+      "content": "diff --git a/lib/claims.py b/lib/claims.py\n--- a/lib/claims.py\n+++ b/lib/claims.py\n@@ -1,6 +1,8 @@\n def release_if_stale(claim, snapshot):\n     owner = snapshot.get_owner(claim.resource_id)\n     if owner is not None and owner != claim.holder:\n         return False\n+    if owner is None and not claim.is_expired():\n+        return False\n     claim.release()\n     return True\ndiff --git a/tests/test_claims.py b/tests/test_claims.py\n--- a/tests/test_claims.py\n+++ b/tests/test_claims.py\n@@ -1,4 +1,10 @@\n def test_release_denied_for_mismatched_owner():\n     claim = Claim(holder=\"worker-a\", resource_id=\"r1\")\n     snapshot = FakeSnapshot(owners={\"r1\": \"worker-b\"})\n     assert release_if_stale(claim, snapshot) is False\n+\n+\n+def test_release_denied_when_owner_absent_and_not_expired():\n+    claim = Claim(holder=\"worker-a\", resource_id=\"r1\", expired=False)\n+    snapshot = FakeSnapshot(owners={})\n+    assert release_if_stale(claim, snapshot) is False\n"
+    }
+  },
+  "change_contract": {
+    "goal": "Prevent release_if_stale from releasing a claim whose snapshot owner is transiently absent unless the claim has actually expired.",
+    "acceptance_criteria": ["release_if_stale denies release when the snapshot owner is absent and the claim has not expired.", "release_if_stale still denies release when a different owner holds the claim."],
+    "non_goals": ["Change how or when a claim expires."],
+    "preserved_behaviors": ["release_if_stale still denies release when the snapshot owner does not match the claim holder."]
+  },
+  "sources": {
+    "repository_instructions": [],
+    "named_documents": [{"label": "Claim release guard", "location": "docs/CLAIMS.md", "summary": "A stale claim may only be released once its snapshot ownership is confirmed absent or the claim itself has expired."}],
+    "nearby_patterns": []
+  },
+  "validation": [
+    {"name": "claims tests", "command": "pytest tests/test_claims.py", "scope": "focused", "status": "passed", "result": "2 passed"},
+    {"name": "full tests", "command": "pytest", "scope": "full", "status": "passed", "result": "41 passed"}
+  ]
+}

review-suite/scripts/evals/calibration.py

@@ -88,7 +88,7 @@ def kinds(self) -> frozenset[str]:
 def probe_result(probe: dict[str, Any], candidate: dict[str, Any]) -> dict[str, Any]:
     """Render one probe as a review result bound to the case's candidate."""
     return {
-        "schema_version": "1.2",
+        "schema_version": "1.3",
         "lens": "aggregate",
         "candidate": candidate,
         "verdict": probe["verdict"],

review-suite/scripts/evals/fixture_executor.py

@@ -88,7 +88,7 @@ def _clean_lens_executions(candidate: dict[str, Any]) -> list[dict[str, Any]]:
 
 def _review(candidate: dict[str, Any], verdict: str, findings: list[dict[str, Any]]):
     result = {
-        "schema_version": "1.2",
+        "schema_version": "1.3",
         "lens": "aggregate",
         "candidate": dict(candidate),
         "verdict": verdict,