Bind LLM-proposed claims to changed tests behind two mechanical gates

DESIGN.md

@@ -220,12 +220,14 @@ operationally: **the capped diff — your source changes — is transmitted to t
 Anthropic API.** Nothing else leaves the machine, and nothing at all does
 without the flag.
 
-The cardinal rule is structural here, not aspirational: **proposals carry no
-probes**, land in the remainder at T0, and are marked `[llm-proposed]` in
-every rendering — nothing the model says can raise a tier or produce a false
-pass. The worst a hallucinated claim can do is waste a remainder row. What the
-extractor buys is an honest remainder for changes that never stated their
-claims: "this change implicitly asserts X, Y, Z — none of it checked."
+The cardinal rule is structural here, not aspirational: **nothing the model
+says can, by itself, raise a tier or produce a false pass.** A proposal is
+minted probe-less, lands in the remainder at T0, and is marked
+`[llm-proposed]` in every rendering — verification included, so the
+provenance is never laundered away. The worst a hallucinated claim can do is
+waste a remainder row. What the extractor buys is an honest remainder for
+changes that never stated their claims: "this change implicitly asserts X,
+Y, Z — none of it checked."
 
 Discipline: pinned model (`claude-sonnet-5`; `CORRECTFUL_LLM_MODEL`
 overrides), a strict JSON output contract that fails loudly on
@@ -240,9 +242,43 @@ mechanical path, so the CI gate never depends on a model.
 ANTHROPIC_API_KEY=... correctful -base auto -llm
 ```
 
-Verifying LLM proposals (binding them to probes) is a later increment, gated
-like every extractor before it: kept only if it raises verification without a
-false bind.
+### Model-proposed edges (schema 0.0.8): proof-carrying binding for LLM claims
+
+Verifying LLM proposals is where the value loop closes — and where the trust
+risk concentrates: a wrong claim→test association plus a passing test would
+mint a false verification, the one failure mode the product exists to
+prevent. So the model is allowed to propose an EDGE, never to certify one.
+A proposal may name, in an optional `test` field, a changed Go test that
+directly checks the claim, and the edge must then survive two mechanical
+gates:
+
+1. **Existence, at mint time.** The named test's definition must appear in
+   the diff the model was shown — an added or context line of a changed
+   `_test.go` file (a deleted definition does not count: the test no longer
+   exists to run). Exactly one changed test file may define it (an ambiguous
+   name fails closed), and the claim's own file must be shipped Go code —
+   the target the second gate will check. A failed edge mints the claim
+   probe-less, exactly as before; the claim is never rejected for a bad
+   edge.
+2. **Execution, at run time.** The bound probe's run is instrumented for
+   coverage, and the pass counts for the LLM claim ONLY when the profile
+   shows execution reaching the claim's file (`binding: file-covered` — the
+   file-level analogue of the function-level coverage-proven binding that
+   annotated spec-id claims get; an LLM claim carries a file, never a line).
+   Fail-closed in both directions: a profile whose execution never touched
+   the file REFUTES the edge (`file-not-reached` — which says nothing about
+   the claim itself), and a pass with no profile at all raises nothing. The
+   remainder row discloses which gate discarded the pass.
+
+Refutation keeps its unconditional dominance: a failing test in the change
+blocks the gate no matter whose edge bound it — a mis-attributed refutation
+is fail-safe, because the failure itself is real. What the model's word can
+now reach, end to end: a remainder row becomes a T1 verified row exactly
+when a machine confirmed both that the named test exists in the change and
+that its execution demonstrably touches the code the claim is about — still
+not proof the test asserts the right property, and the receipt's
+`[llm-proposed]` marker plus `[binding: file-coverage-proven]` state
+precisely that trust boundary on the row itself.
 
 Measured (first live runs, 2026-08): on a wild-case diff — a real 19-file
 change with zero pre-written claims — 19 of 20 proposals were accurate,

README.md

@@ -18,8 +18,9 @@ Three rules control the receipt:
 
 - **A refuted claim stops the merge.** One failed probe is stronger than many
   passed probes.
-- **Only a machine can verify a claim.** An LLM can propose a claim. A
-  proposal cannot increase a tier.
+- **Only a machine can verify a claim.** An LLM can propose a claim, and it
+  can point to a changed test. The pass counts only when coverage data shows
+  that the test runs the claim's file.
 - **The receipt always shows the remainder**, also when the remainder is
   empty. The receipt also shows its own blind spots: the files that no
   harvester read, and the files that the scope excluded.
@@ -86,7 +87,8 @@ remainder is a report, not a defect.
 
 Note: The `-llm` option sends the capped diff — your source changes — to the
 Anthropic API. The option needs `ANTHROPIC_API_KEY`. Without the option, no
-data goes out from your machine. LLM proposals stay in the remainder at T0.
+data goes out from your machine. An LLM proposal stays in the remainder,
+unless a coverage-checked test in the change verifies it.
 
 ## The merge gate
 
@@ -112,7 +114,7 @@ This repository uses this gate for each of its own pull requests.
 | an Alloy `run` | a witness claim (a pass shows that the model is consistent) | the Alloy result file | T3 |
 | spec ids in shipped code (`INV-…`, `AP-…`, …) | a reference claim, anchored to its definition | id-named tests, with coverage proof | — |
 | MUST clauses in a normative document | a must-clause claim | no probe is available — the claim stays in the remainder | T0 |
-| nothing (`-llm`) | LLM proposals, with the mark `[llm-proposed]` | no probe, by design | T0 |
+| nothing (`-llm`) | LLM proposals, with the mark `[llm-proposed]` | a changed test, only when the model names it and coverage confirms the link | T0 or T1 |
 
 The tiers: **T0** unverified · **T1** one assertion held · **T2** an
 accept/reject pair held · **T3** property or model check · **T4** proof,

internal/llmextract/llmextract.go

@@ -3,12 +3,17 @@
 // implicitly — the wild case, where nobody wrote a test name, a spec id, or a
 // MUST clause for the checker to harvest.
 //
-// The cardinal rule is structural here, not aspirational: proposed claims are
-// minted with NO probes, so they land in the receipt's remainder at T0 and
-// nothing the model says can raise a tier or produce a false pass. The worst
-// a hallucinated claim can do is waste a remainder row, and every proposal is
-// marked llm-proposed so a reader never mistakes it for something the change
-// wrote down itself.
+// The cardinal rule is structural here, not aspirational: nothing the model
+// says can, BY ITSELF, raise a tier or produce a false pass. A proposed claim
+// is minted probe-less and lands in the remainder — unless the model also
+// names a changed test that checks it, and that EDGE survives two mechanical
+// gates: the test must exist in the diff (a changed _test.go function, found
+// by parsing the sections the model was shown), and at run time the probe's
+// own coverage profile must show execution reaching the claim's file. An edge
+// that fails either gate binds nothing or verifies nothing; the receipt
+// discloses which gate rejected it. The worst a hallucinated claim can do is
+// waste a remainder row, and every proposal is marked llm-proposed so a
+// reader never mistakes it for something the change wrote down itself.
 //
 // Determinism discipline: pinned model (overridable via CORRECTFUL_LLM_MODEL),
 // a strict JSON output contract with schema validation, and
@@ -24,6 +29,7 @@ import (
 	"io"
 	"net/http"
 	"os"
+	"regexp"
 	"strings"
 	"time"
 
@@ -98,7 +104,7 @@ func (h Harvester) Harvest(repoDir string, files []string) (harvest.Result, erro
 	if err != nil {
 		return harvest.Result{}, fmt.Errorf("llm extraction: %w", err)
 	}
-	claims, err := mintProposals(raw, read)
+	claims, err := mintProposals(raw, read, sent)
 	if err != nil {
 		return harvest.Result{}, fmt.Errorf("llm extraction: %w", err)
 	}
@@ -177,11 +183,13 @@ func sectionFile(sec string) string {
 	return ""
 }
 
-// proposal is the model's required output element.
+// proposal is the model's required output element. Test is optional: the name
+// of a changed Go test function that directly checks the claim.
 type proposal struct {
 	Shape string `json:"shape"`
 	File  string `json:"file"`
 	Text  string `json:"text"`
+	Test  string `json:"test"`
 }
 
 // allowedShapes is the claim taxonomy the model may use — anything else is
@@ -206,9 +214,10 @@ Rules:
 2. Write each claim as one plain declarative sentence about the changed code.
 3. Attribute each claim to the single changed file it is most about, using the exact path shown in the diff.
 4. Propose at most ` + fmt.Sprint(maxProposals) + ` claims — the most load-bearing ones. If the diff supports fewer, return fewer. Do not invent claims the diff does not support.
+5. If a Go test function CHANGED IN THIS DIFF directly checks a claim, add its exact function name in a "test" field. Only name a test whose definition appears in the diff. Omit the field when no changed test checks the claim or you are not sure.
 
 Output: a JSON array only — no prose, no code fences. Each element:
-{"shape": "<one of: assertion, invariant, must-clause, coupled-fields-lockstep, safety-assert, witness>", "file": "<changed file path>", "text": "<one sentence>"}
+{"shape": "<one of: assertion, invariant, must-clause, coupled-fields-lockstep, safety-assert, witness>", "file": "<changed file path>", "text": "<one sentence>", "test": "<optional: TestXxx changed in this diff>"}
 
 The diff:
 
@@ -222,14 +231,23 @@ The diff:
 	return b.String()
 }
 
-// mintProposals validates the model's output and mints probe-less claims.
-// Malformed output fails LOUDLY — a parse gate, not a salvage operation; the
-// only tolerated wrapper is a markdown code fence.
-func mintProposals(raw string, readFiles []string) ([]schema.Claim, error) {
+// mintProposals validates the model's output and mints claims. Malformed
+// output fails LOUDLY — a parse gate, not a salvage operation; the only
+// tolerated wrapper is a markdown code fence.
+//
+// A proposal naming a "test" binds a go-test probe ONLY when the existence
+// gate passes: the test's definition appears in the diff sections the model
+// was shown (deleted definitions do not count), exactly one changed _test.go
+// file defines it, and the claim's own file is a non-test Go file — the
+// target the run-time coverage gate will check execution against. A binding
+// that fails any of these mints the claim probe-less, exactly as before; the
+// CLAIM is never rejected for a bad edge.
+func mintProposals(raw string, readFiles []string, sections []string) ([]schema.Claim, error) {
 	inRead := make(map[string]bool, len(readFiles))
 	for _, f := range readFiles {
 		inRead[f] = true
 	}
+	testDefs := testDefsInSections(sections)
 	var props []proposal
 	if err := json.Unmarshal([]byte(stripFences(raw)), &props); err != nil {
 		return nil, fmt.Errorf("model output is not the required JSON array: %v (output begins %q)", err, truncateStr(raw, 120))
@@ -245,6 +263,12 @@ func mintProposals(raw string, readFiles []string) ([]schema.Claim, error) {
 		if len(claims) == maxProposals {
 			break
 		}
+		var probes []string
+		if name := strings.TrimSpace(p.Test); name != "" {
+			if file, ok := testDefs[name]; ok && file != "" && isBindableClaimFile(p.File) {
+				probes = []string{schema.GoTestProbeID(file, name)}
+			}
+		}
 		claims = append(claims, schema.Claim{
 			// The id hashes the proposal's content, so it is stable across
 			// reorderings and re-runs of the same proposal — an ordinal would
@@ -257,13 +281,52 @@ func mintProposals(raw string, readFiles []string) ([]schema.Claim, error) {
 				File: p.File,
 				Ref:  "llm",
 			},
-			// No probes, by design: a proposal is remainder-bound until a
-			// machine verifies it.
+			// A model-proposed probe binding is an EDGE PROPOSAL, not
+			// verification: at run time the probe only counts for this claim
+			// when its coverage profile shows execution reaching Source.File
+			// (see probe.Dispatch and receipt weighing). Probe-less remains
+			// the default: a proposal is remainder-bound until a machine
+			// verifies it.
+			ProbeIDs: probes,
 		})
 	}
 	return claims, nil
 }
 
+// isBindableClaimFile reports whether a claim file is a target the coverage
+// gate can check: shipped Go code, not a test file.
+func isBindableClaimFile(f string) bool {
+	return strings.HasSuffix(f, ".go") && !strings.HasSuffix(f, "_test.go")
+}
+
+// testDefRe matches a top-level Go test function definition on an added or
+// context diff line (leading '+' or ' '). A deleted definition ('-') must not
+// match: the test no longer exists to run.
+var testDefRe = regexp.MustCompile(`(?m)^[+ ]func (Test[A-Za-z0-9_]*)\s*\(`)
+
+// testDefsInSections maps each Go test function name defined in a changed
+// _test.go section to that section's file. A name defined in MORE than one
+// changed test file maps to "" — ambiguous, so the existence gate fails
+// closed rather than guessing which package the model meant.
+func testDefsInSections(sections []string) map[string]string {
+	defs := map[string]string{}
+	for _, sec := range sections {
+		file := sectionFile(sec)
+		if !strings.HasSuffix(file, "_test.go") {
+			continue
+		}
+		for _, m := range testDefRe.FindAllStringSubmatch(sec, -1) {
+			name := m[1]
+			if prev, seen := defs[name]; seen && prev != file {
+				defs[name] = ""
+				continue
+			}
+			defs[name] = file
+		}
+	}
+	return defs
+}
+
 // fnv32 is FNV-1a over the string — a stable content id, not a security hash.
 func fnv32(s string) uint32 {
 	h := uint32(2166136261)

internal/llmextract/llmextract_test.go

@@ -289,3 +289,113 @@ func TestGithubSectionCannotCrowdOutCode(t *testing.T) {
 		t.Error("shipped-code sections missing")
 	}
 }
+
+// bindingPatch extends the sample with two changed test files (git's exact
+// framing; content synthetic): one new test, one deleted test, one context
+// test, and a name defined in BOTH test files (ambiguous).
+const bindingPatch = samplePatch + `diff --git a/pkg/gate/gate_test.go b/pkg/gate/gate_test.go
+index 5555555..6666666 100644
+--- a/pkg/gate/gate_test.go
++++ b/pkg/gate/gate_test.go
+@@ -1,8 +1,11 @@
+ package gate
+
++func TestCheckRejectsNil(t *testing.T) {
++	if Check(nil) {
++		t.Fatal("nil accepted")
++	}
++}
+-func TestGoneCheck(t *testing.T) {
+-	t.Skip()
+-}
+ func TestContextCheck(t *testing.T) {
+ 	_ = Check
+ }
++func TestDupName(t *testing.T) {
++	_ = Check
++}
+diff --git a/pkg/other/other_test.go b/pkg/other/other_test.go
+index 7777777..8888888 100644
+--- a/pkg/other/other_test.go
++++ b/pkg/other/other_test.go
+@@ -1,3 +1,6 @@
+ package other
+
++func TestDupName(t *testing.T) {
++	_ = 1
++}
+`
+
+// TestLLMEdgeExistenceGate: a proposal's "test" binds a go-test probe ONLY
+// when the diff itself proves the test exists — a changed _test.go defines it
+// on an added or context line, exactly one file defines it, and the claim's
+// file is shipped Go code. Every failing case mints the claim PROBE-LESS; the
+// claim itself is never rejected for a bad edge.
+func TestLLMEdgeExistenceGate(t *testing.T) {
+	sections := splitSections(bindingPatch)
+	readFiles := []string{"pkg/gate/gate.go", "pkg/gate/gate_test.go", "docs/notes.md"}
+	cases := []struct {
+		name      string
+		file      string
+		test      string
+		wantProbe string
+	}{
+		{"added test binds", "pkg/gate/gate.go", "TestCheckRejectsNil",
+			"go-test:pkg/gate/gate_test.go:TestCheckRejectsNil"},
+		{"context test binds", "pkg/gate/gate.go", "TestContextCheck",
+			"go-test:pkg/gate/gate_test.go:TestContextCheck"},
+		{"deleted test does not exist", "pkg/gate/gate.go", "TestGoneCheck", ""},
+		{"test absent from diff", "pkg/gate/gate.go", "TestNowhere", ""},
+		{"ambiguous across test files", "pkg/gate/gate.go", "TestDupName", ""},
+		{"non-go claim file unbindable", "docs/notes.md", "TestCheckRejectsNil", ""},
+		{"test-file claim unbindable", "pkg/gate/gate_test.go", "TestCheckRejectsNil", ""},
+		{"no test field", "pkg/gate/gate.go", "", ""},
+	}
+	for _, tc := range cases {
+		t.Run(tc.name, func(t *testing.T) {
+			raw := fmt.Sprintf(`[{"shape":"assertion","file":%q,"text":"a claim.","test":%q}]`, tc.file, tc.test)
+			claims, err := mintProposals(raw, readFiles, sections)
+			if err != nil {
+				t.Fatal(err)
+			}
+			if len(claims) != 1 {
+				t.Fatalf("claims = %d, want 1 (the claim survives a bad edge)", len(claims))
+			}
+			got := ""
+			if len(claims[0].ProbeIDs) == 1 {
+				got = claims[0].ProbeIDs[0]
+			}
+			if got != tc.wantProbe {
+				t.Errorf("probe = %q, want %q", got, tc.wantProbe)
+			}
+		})
+	}
+}
+
+// TestLLMEdgeFlowsThroughHarvest: the binding survives the full Harvest path
+// — fixture server, parse gate, minting — so a bound proposal reaches the
+// dispatcher with its probe attached and its llm-proposed source intact.
+func TestLLMEdgeFlowsThroughHarvest(t *testing.T) {
+	out := `[{"shape":"invariant","file":"pkg/gate/gate.go","text":"Check rejects nil input.","test":"TestCheckRejectsNil"}]`
+	client, _, _ := fixtureServer(t, 200, apiFixture(out))
+	h := Harvester{Patch: bindingPatch, Client: client}
+
+	res, err := h.Harvest("/nowhere", []string{"pkg/gate/gate.go", "pkg/gate/gate_test.go", "docs/notes.md"})
+	if err != nil {
+		t.Fatal(err)
+	}
+	if len(res.Claims) != 1 {
+		t.Fatalf("claims = %d, want 1", len(res.Claims))
+	}
+	c := res.Claims[0]
+	if c.Source.Kind != schema.SourceLLM {
+		t.Errorf("source kind = %q, want llm", c.Source.Kind)
+	}
+	want := "go-test:pkg/gate/gate_test.go:TestCheckRejectsNil"
+	if len(c.ProbeIDs) != 1 || c.ProbeIDs[0] != want {
+		t.Errorf("probes = %v, want [%s]", c.ProbeIDs, want)
+	}
+	if !strings.Contains(extractionPrompt(splitSections(bindingPatch)), `"test"`) {
+		t.Errorf("prompt does not describe the optional test field")
+	}
+}