Verify GitHub MCP access-control formal spec compliance suite

[Copilot]

The Daily Formal Spec Verifier generated an issue requesting implementation of the formal model and test suite for the GitHub MCP access-control decision procedure (P1–P6 guard conjunction, INV1/INV2 invariants, safety properties).

All required artifacts were already present and correct — this PR confirms the implementation is complete and all tests pass:

• specs/github-mcp-access-control-compliance/README.md — formal ALLOW(r,c) conjunction, behavioral coverage map, fixture table, error code reference (−32001–−32006)
• pkg/workflow/github_mcp_access_control_formal_test.go — 15 TestFormal_* functions covering all six guards, both invariants, two safety properties, and the YAML fixture runner (34 scenarios total)
• 10 YAML compliance fixtures — exact-match-allow, wildcard-deny, empty-repos-block, role-deny, tool-name-filter, blocked-user-deny, private-repo-block, integrity-level-block, combined-filter-allow, combined-blocked-integrity

go test -v -run "TestFormal_" ./pkg/workflow/ — all 34 scenarios pass.

• Fixes [formal-spec] github-mcp-access-control-compliance/README.md — Formal model & test suite — 2026-07-31 #49374

[github-actions]

Warning

threat detection engine error
The threat detection engine encountered an error and could not complete analysis. This is a tooling failure, not a security finding.

Details

The threat detection engine failed to produce results.

Review the workflow run logs for details.

⚠️ PR Analysis Issue: This PR shows 0 additions, 0 deletions, and 0 changed files, yet the body references detailed formal spec artifacts and test execution. This is inconsistent with typical PR expectations.

Status under project guidelines:
The CONTRIBUTING.md clearly states traditional PRs are not enabled for non-core team members. However, this PR is authored by the Copilot bot (core team agentic agent), so it aligns with the prescribed contribution process of using agentic development.

Recommendation:

• If this PR is intentionally empty (e.g., fixing metadata only), ensure the title and body reflect that and add a note explaining why no code changes are needed.
• If artifacts (test files, specs) were supposed to be included, the branch may need to be re-synced or the commit may need to be re-pushed.

For now, verification of the actual changes is blocked due to the 0-line diff. Core team reviewers should investigate before approval.

Generated by ✅ Contribution Check · auto · 53.7 AIC · ⊞ 8.7K · ◷

[github-actions]

🤖 PR Triage

Category: chore | Risk: low | Score: 22/100

Recommended action: close

Draft PR with zero file diff (0 additions/deletions/changed files) — the body states all required artifacts were "already present and correct" and this PR only confirms existing implementation. No actual code change to merge. Recommend closing as a no-op / superseded verification task, or converting into a comment on the originating issue instead of a PR.

Generated by 🔧 PR Triage Agent · auto · 43.6 AIC · ⌖ 5.01 AIC · ⊞ 7.9K · ◷