feat: add GitHub Copilot SDK backend - #3167
Conversation
There was a problem hiding this comment.
Graphify reviewed this change.
Worth a look — the grounded gate found no coupling regressions or blocking issues, but 2 advisory finding(s) below merit a look before merge.
Formal verification. 6 change(s) tested, no difference found (not proven).
Graphify review — findings
Adds an optional copilot-sdk semantic-extraction backend that runs each request through a fresh, isolated Copilot SDK session in mode="empty" — no tools, MCP, persistence, telemetry, or fallback to another provider — reading existing login from COPILOT_HOME while using temporary working/config paths. Model selection follows --model then GRAPHIFY_COPILOT_SDK_MODEL/GRAPHIFY_COPILOT_MODEL/COPILOT_MODEL, requests run serially unless GRAPHIFY_COPILOT_SDK_PARALLEL=1, and a post-dispatch failure is reported as an unknown outcome rather than replayed. Wires it through the CLI backend dispatch, documents env vars and setup in the README and a new backend doc, and adds a cross-platform CI job exercising the Copilot contract plus dedup/labeling/PR tests.
Worth a look
- primary is referenced in finally before assignment on early exception paths —
graphify/copilot_sdk_backend.py· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- record_cleanup_failure only sets primary via BaseException but primary may be undefined in finally when no exception raised —
graphify/copilot_sdk_backend.py· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 1713 functions depend on the 1261 functions this change touches.
Health — this change adds coupling hotspots:
- new:
deduplicate_entities()— 64 callers, 21 callees - new:
build_merge()— 46 callers, 14 callees - new:
extract_files_direct()— 20 callers, 23 callees - new:
_extract_with_adaptive_retry()— 25 callers, 13 callees - new:
_call_claude_cli()— 31 callers, 10 callees - new:
_call_llm()— 14 callers, 22 callees - new:
extract_corpus_parallel()— 26 callers, 11 callees - new:
dispatch_command()— 2 callers, 123 callees - …and 31 more — each is listed as a finding
Verification — 1713 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 1687 function(s) in the blast radius were not formally verified this run
Formal verification
Could not verify: Could not verify build\_merge.
The verifier did not have enough to check build\_merge, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `graph_path` is annotated `str | Path | None` — outside the synthesizable primitive/collection set
No difference found (not proven): No behavior difference found in \_flush\_stat\_index (not a proof).
The verifier ran both versions of \_flush\_stat\_index on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
Could not verify: Could not verify dispatch\_command.
The verifier did not have enough to check dispatch\_command, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly SystemExit — names the real obstacle, not a sampling gap)
No difference found (not proven): No behavior difference found in \_partition (not a proof).
The verifier ran both versions of \_partition on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
Could not verify: Could not verify \_llm\_tiebreak.
The verifier did not have enough to check \_llm\_tiebreak, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 200 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify extract\_commonlisp.
The verifier did not have enough to check extract\_commonlisp, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify extract\_elixir.
The verifier did not have enough to check extract\_elixir, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_extract\_generic.
The verifier did not have enough to check \_extract\_generic, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_build\_image\_refs.
The verifier did not have enough to check \_build\_image\_refs, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_call\_llm.
The verifier did not have enough to check \_call\_llm, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify \_default\_model\_for\_backend.
The verifier did not have enough to check \_default\_model\_for\_backend, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly KeyError — names the real obstacle, not a sampling gap)
No difference found (not proven): No behavior difference found in detect\_backend (not a proof).
The verifier ran both versions of detect\_backend on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
Could not verify: Could not verify extract\_corpus\_parallel.
The verifier did not have enough to check extract\_corpus\_parallel, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify extract\_files\_direct.
The verifier did not have enough to check extract\_files\_direct, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_extract\_with\_adaptive\_retry.
The verifier did not have enough to check \_extract\_with\_adaptive\_retry, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_image\_notes.
The verifier did not have enough to check \_image\_notes, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: non-vacuity: domain too small (only 1 distinct inputs exercised, need 3) — 'no divergence' would be near-vacuous
Could not verify: Could not verify label\_communities.
The verifier did not have enough to check label\_communities, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 49 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify \_merge\_into.
The verifier did not have enough to check \_merge\_into, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 6 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly KeyError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify \_read\_files.
The verifier did not have enough to check \_read\_files, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `units` is annotated `'list[Path | FileSlice]'` — outside the synthesizable primitive/collection set
No difference found (not proven): No behavior difference found in \_with\_image\_notes (not a proof).
The verifier ran both versions of \_with\_image\_notes on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
No difference found (not proven): No behavior difference found in \_run\_cli (not a proof).
The verifier ran both versions of \_run\_cli on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
No difference found (not proven): No behavior difference found in triage\_with\_opus (not a proof).
The verifier ran both versions of triage\_with\_opus on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
· 3 grounded finding(s) anchored inline below; 36 more finding(s) on lines outside this diff (see the check run).
| raise asyncio.TimeoutError | ||
|
|
||
|
|
||
| async def _call_once( |
There was a problem hiding this comment.
_call_once()
fans out to 10 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return pool.submit(run_isolated).result() | ||
|
|
||
|
|
||
| def call_copilot_sdk( |
There was a problem hiding this comment.
call_copilot_sdk()
high coupling complexity (Ca·Ce = 16).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return _with_attempt_usage(merged, result) | ||
|
|
||
|
|
||
| def extract_corpus_parallel( |
There was a problem hiding this comment.
extract_corpus_parallel()
fans out to 11 callees (efferent coupling); 26 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
There was a problem hiding this comment.
Graphify reviewed this change.
Worth a look — the grounded gate found no coupling regressions or blocking issues, but 5 advisory finding(s) below merit a look before merge.
Formal verification. 4 change(s) tested, no difference found (not proven).
Graphify review — findings
Adds an optional copilot-sdk semantic-extraction backend that runs each request in a fresh, isolated no-tool Copilot SDK session reusing the user's existing GitHub Copilot login, with inline-image support, configurable model/reasoning/context-tier via env vars, and serial execution unless GRAPHIFY_COPILOT_SDK_PARALLEL=1. The backend is never auto-selected and never falls back to another provider; a post-dispatch failure is surfaced as an unknown outcome rather than replayed, and it records SDK token usage plus the premium-request multiplier without converting it to a USD claim. Wires it through the CLI, docs, and README, and gives it a dedicated copilot-backend CI job that installs the copilot extra and runs the focused contract across Ubuntu, macOS, and Windows.
Worth a look
- _image_notes uses unsupported file_attachments parameter —
graphify/llm.py:1057· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Copilot SDK backend requires API key by default, blocking runtime-authenticated use —
graphify/llm.py:2171· Escalate · high- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Copilot SDK availability check can import attacker-controlled copilot.py from the working directory —
graphify/cli.py:3556· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Synchronous abort failure masks the bounded operation timeout —
graphify/copilot_sdk_backend.py:245· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
- Abort cleanup task can leak after timeout —
graphify/copilot_sdk_backend.py:273· Escalate · medium- agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 1727 functions depend on the 1263 functions this change touches.
Health — this change adds coupling hotspots:
- new:
deduplicate_entities()— 64 callers, 21 callees - new:
build_merge()— 53 callers, 13 callees - new:
extract_files_direct()— 20 callers, 23 callees - new:
_extract_with_adaptive_retry()— 25 callers, 13 callees - new:
_call_claude_cli()— 31 callers, 10 callees - new:
_call_llm()— 14 callers, 22 callees - new:
extract_corpus_parallel()— 26 callers, 11 callees - new:
dispatch_command()— 2 callers, 123 callees - …and 31 more — each is listed as a finding
Verification — 1727 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 1701 function(s) in the blast radius were not formally verified this run
Formal verification
Could not verify: Could not verify dispatch\_command.
The verifier did not have enough to check dispatch\_command, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly SystemExit — names the real obstacle, not a sampling gap)
Could not verify: Could not verify \_llm\_tiebreak.
The verifier did not have enough to check \_llm\_tiebreak, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 200 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify \_build\_image\_refs.
The verifier did not have enough to check \_build\_image\_refs, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_call\_llm.
The verifier did not have enough to check \_call\_llm, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify \_default\_model\_for\_backend.
The verifier did not have enough to check \_default\_model\_for\_backend, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly KeyError — names the real obstacle, not a sampling gap)
No difference found (not proven): No behavior difference found in detect\_backend (not a proof).
The verifier ran both versions of detect\_backend on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
Could not verify: Could not verify extract\_corpus\_parallel.
The verifier did not have enough to check extract\_corpus\_parallel, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify extract\_files\_direct.
The verifier did not have enough to check extract\_files\_direct, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_extract\_with\_adaptive\_retry.
The verifier did not have enough to check \_extract\_with\_adaptive\_retry, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set
Could not verify: Could not verify \_image\_notes.
The verifier did not have enough to check \_image\_notes, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: non-vacuity: domain too small (only 1 distinct inputs exercised, need 3) — 'no divergence' would be near-vacuous
Could not verify: Could not verify label\_communities.
The verifier did not have enough to check label\_communities, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 49 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify \_merge\_into.
The verifier did not have enough to check \_merge\_into, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 6 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly KeyError — names the real obstacle, not a sampling gap)
Could not verify: Could not verify \_read\_files.
The verifier did not have enough to check \_read\_files, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: parameter `units` is annotated `'list[Path | FileSlice]'` — outside the synthesizable primitive/collection set
No difference found (not proven): No behavior difference found in \_with\_image\_notes (not a proof).
The verifier ran both versions of \_with\_image\_notes on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
No difference found (not proven): No behavior difference found in \_run\_cli (not a proof).
The verifier ran both versions of \_run\_cli on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
No difference found (not proven): No behavior difference found in triage\_with\_opus (not a proof).
The verifier ran both versions of triage\_with\_opus on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
· 3 grounded finding(s) anchored inline below; 36 more finding(s) on lines outside this diff (see the check run).
| raise asyncio.TimeoutError | ||
|
|
||
|
|
||
| async def _call_once( |
There was a problem hiding this comment.
_call_once()
fans out to 10 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return pool.submit(run_isolated).result() | ||
|
|
||
|
|
||
| def call_copilot_sdk( |
There was a problem hiding this comment.
call_copilot_sdk()
high coupling complexity (Ca·Ce = 16).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| return _with_attempt_usage(merged, result) | ||
|
|
||
|
|
||
| def extract_corpus_parallel( |
There was a problem hiding this comment.
extract_corpus_parallel()
fans out to 11 callees (efferent coupling); 26 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
Summary
This is a smaller replacement for #3136. It keeps the original GitHub Copilot SDK backend and only the three fixes that were reproduced and verified:
The later automated review-loop commits from #3136 are intentionally excluded to keep this change focused and reviewable.
Local verification
v8:372 passed, 1 skippedv8:5,058 passed, 76 skippedgraphify/copilot_sdk_backend.py:0 errors, 0 warningsgit diff --check: passedThe full suite was run with hydrated Git history, the declared
copilotandollamaextras, provider-key environment variables removed, andPYTHONPATHpropagated to subprocess tests.The branch includes a merge of current
v8. Its conflict resolution was compared against a clean replay of the three feature commits; both produced the same Git tree.CI note
This PR comes from a fork. A maintainer may need to approve the GitHub Actions workflow before the upstream matrix can run.
Relationship to #3136
#3136 is preserved and has not been force-pushed or deleted. Once this replacement is accepted, #3136 can be closed as superseded.