From ba4657da5769a77d0a78181873433f772f9d7845 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 23 Jul 2026 16:13:34 +0000
Subject: [PATCH 1/2] Initial plan


From 0d9f0c6941cdb4f562dbeb3e9b5cae04d514c826 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 23 Jul 2026 16:26:24 +0000
Subject: [PATCH 2/2] Align formal access-control spec usage and predicate
 label

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
---
 .../github_mcp_access_control_formal_test.go  |  2 +-
 .../README.md                                 | 23 +++++--------------
 2 files changed, 7 insertions(+), 18 deletions(-)

diff --git a/pkg/workflow/github_mcp_access_control_formal_test.go b/pkg/workflow/github_mcp_access_control_formal_test.go
index ddd9e012f1d..575c50cc858 100644
--- a/pkg/workflow/github_mcp_access_control_formal_test.go
+++ b/pkg/workflow/github_mcp_access_control_formal_test.go
@@ -64,7 +64,7 @@ func TestFormal_WildcardMatch(t *testing.T) {
 }
 
 func TestFormal_OmittedReposAllowAll(t *testing.T) {
-	// P1_RepoMatch: omitted repos field means "no restriction" — all accessible repos are allowed (spec §4.4.1).
+	// P2_RepoMatch: omitted repos field means "no restriction" — all accessible repos are allowed (spec §4.4.1).
 	assert.True(t, formalEvaluateAccess(formalToolConfig{}, formalAccessRequest{Repository: "github/gh-aw"}).allow)
 	assert.True(t, formalEvaluateAccess(formalToolConfig{}, formalAccessRequest{Repository: "microsoft/vscode"}).allow)
 
diff --git a/specs/github-mcp-access-control-compliance/README.md b/specs/github-mcp-access-control-compliance/README.md
index f1fbe4e2ba7..e6b889ae7b0 100644
--- a/specs/github-mcp-access-control-compliance/README.md
+++ b/specs/github-mcp-access-control-compliance/README.md
@@ -123,28 +123,17 @@ and no error is returned.
 4. Update `expected` fields to match the required outcome.
 5. Register the new fixture in the table above and link it from §11.4 of the specification.
 
-## Running Compliance Tests
+## Usage
 
-Compliance tests that consume these fixtures are located in (or will be added to):
-
-```
-pkg/workflow/tools_validation_test.go   — §11.1.1 configuration validation
-pkg/workflow/tools_validation_test.go   — §11.1.8 blocked-user tests
-```
-
-To run all related tests:
-
-```bash
-go test -v -run "TestValidateGitHubGuardPolicy" ./pkg/workflow/
-```
-
-To run the formal conformance test suite (predicate-mapped tests):
+1. Copy or verify the test file at `pkg/workflow/github_mcp_access_control_formal_test.go`.
+2. No stub interfaces are needed — all types and helpers are self-contained in the file.
+3. Run predicate-mapped tests:
 
 ```bash
-go test -v -run "TestFormal_(ExactMatch|WildcardMatch|OmittedRepos|RoleFilter|PrivateRepo|BlockedUser|ToolName|IntegrityLevel|UnknownContent|InvalidMinIntegrity|CombinedFilters|ErrorCode|NoSpurious)" ./pkg/workflow/
+go test -v -run "TestFormal_" ./pkg/workflow/
 ```
 
-To run the YAML fixture runner (drives every scenario from the fixture files above through the formal evaluator):
+4. Run only the fixture runner:
 
 ```bash
 go test -v -run "TestFormal_FixtureRunner" ./pkg/workflow/