[formal-spec] github-mcp-access-control-compliance/README.md — Formal model & test suite — 2026-07-23

[github-actions]

Summary

This report formalizes the GitHub MCP Access Control Compliance Specification, which defines the runtime access-control decision model for GitHub MCP tools. The specification describes six guard predicates (P1–P6) evaluated in a fixed order (tool selection → repository access control → integrity management). The formalization captures all invariants, error codes, and edge cases, and the generated Go testify suite binds each predicate to an executable conformance test — including a YAML-fixture runner that drives every compliance scenario through the formal evaluator.

Specification

• File: specs/github-mcp-access-control-compliance/README.md
• Focus area: GitHub MCP runtime access-control decision engine
• Formal notation used: Z3 / SMT-LIB + TLA+ (mixed)

Formal Model

Predicates and invariants (illustrative notation)

Top-level allow predicate (spec §4.5.3)

-- Z3 / SMT-LIB style
ALLOW(r, c) ≜
  P1_ToolAllowed(r, c)      -- tool selection
  ∧ P2_RepoMatch(r, c)      -- repository scope
  ∧ P3_RoleAllow(r, c)      -- role authorization
  ∧ P4_PrivateRepoAllow(r,c)-- visibility gate
  ∧ P5_NotBlocked(r, c)     -- blocked-user check (integrity management)
  ∧ P6_IntegrityMet(r, c)   -- min-integrity threshold (integrity management)

P1 — Tool selection (spec §4.3)

P1_ToolAllowed(r, c) ≜
  c.allowed_tools = ∅                    -- no restriction: any tool allowed
  ∨ (r.tool_name ≠ ε
     ∧ r.tool_name ∈ c.allowed_tools)    -- named tool must be present
-- ε (empty tool name) against non-empty list → deny(-32001)

P2 — Repository match (spec §4.4.1)

P2_RepoMatch(r, c) ≜
  c.repos = nil                          -- omitted: allow all accessible repos
  ∨ (c.repos ≠ ∅                         -- empty = compile-time error; runtime: deny
     ∧ ∃ p ∈ c.repos .
         matchPattern(p, r.repository))

matchPattern(p, repo) ≜
  p = "*/*"                              -- full wildcard
  ∨ owner(p) = "*" ∧ name(p) = name(repo)  -- */name
  ∨ owner(p) = owner(repo) ∧ name(p) = "*" -- owner/*
  ∨ p = repo                             -- exact

P3 — Role authorization (spec §4.4.2)

P3_RoleAllow(r, c) ≜
  c.roles = ∅                            -- no restriction: all roles allowed
  ∨ r.user_role ∈ c.roles               -- OR-logic over configured roles
-- deny(-32003) if c.roles ≠ ∅ ∧ r.user_role ∉ c.roles

P4 — Private repository visibility (spec §4.4.3)

P4_PrivateRepoAllow(r, c) ≜
  c.private_repos ≠ false               -- nil or true: private repos allowed
  ∨ ¬r.is_private                       -- public repo always allowed
-- deny(-32004) if c.private_repos = false ∧ r.is_private

P5 — Blocked user (spec §4.5.1, integrity management)

P5_NotBlocked(r, c) ≜
  r.user_login ∉ c.blocked_users
-- deny(-32005) if r.user_login ∈ c.blocked_users
-- evaluated BEFORE P6 in evaluation order

P6 — Integrity level (spec §4.5.2, integrity management)

IntegrityRank : ContentIntegrity → Z
  none       ↦ 0
  unapproved ↦ 1
  approved   ↦ 2
  merged     ↦ 3
  unknown    ↦ -1  -- fail-safe: below any valid threshold

P6_IntegrityMet(r, c) ≜
  c.min_integrity = ε               -- no threshold configured
  ∨ (IntegrityRank(c.min_integrity) ≥ 0    -- config must be recognized
     ∧ IntegrityRank(r.content_integrity)   -- content must be at/above threshold
       ≥ IntegrityRank(c.min_integrity))
-- deny(-32006) otherwise (including unrecognized min_integrity config = fail-safe)

INV1 — Combined allow invariant

-- TLA+ style
INV1_CombinedAllow ==
  ∀ r ∈ AccessRequest, c ∈ ToolConfig .
    Decision(r,c) = allow
    ⟺ P1(r,c) ∧ P2(r,c) ∧ P3(r,c) ∧ P4(r,c) ∧ P5(r,c) ∧ P6(r,c)

INV2 — First-failing guard determines error code

INV2_ErrorCode ==
  ∀ r, c .
    Decision(r,c) = deny(code)
    ⟹ code = errorCode(min{ i ∈ {1..6} | ¬Pi(r,c) })

SAFETY_BlockedUserAlwaysDenied

SAFETY_BlockedUserAlwaysDenied ==
  □ ∀ r, c .
    (P1(r,c) ∧ P2(r,c) ∧ P3(r,c) ∧ P4(r,c) ∧ r.user_login ∈ c.blocked_users)
    ⟹ Decision(r,c) = deny(-32005)

SAFETY_NoSpuriousAllow

SAFETY_NoSpuriousAllow ==
  □ ∀ r, c .
    (¬P1(r,c) ∨ ¬P2(r,c) ∨ ¬P3(r,c) ∨ ¬P4(r,c) ∨ ¬P5(r,c) ∨ ¬P6(r,c))
    ⟹ Decision(r,c) ≠ allow

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
P1_ToolAllowed	TestFormal_ToolNameFilter	allowed-tools allows named tool; empty tool name or unlisted tool denies with -32001
P2_RepoMatch (exact)	TestFormal_ExactMatchAllow	Exact owner/repo pattern allows matching repo, denies others with -32002
P2_RepoMatch (wildcard)	TestFormal_WildcardMatch	owner/*, */repo, and */* patterns evaluated correctly
P2_RepoMatch (omitted)	TestFormal_OmittedReposAllowAll	Omitted repos allows all repos; empty array treated as no-match
P3_RoleAllow	TestFormal_RoleFilter	Role OR-logic: matching role allows, insufficient role denies with -32003
P4_PrivateRepoAllow	TestFormal_PrivateRepoControl	private-repos: false blocks private repos; public repos unaffected
P5_NotBlocked	TestFormal_BlockedUserDeny	Blocked user denied within integrity management with -32005
P6_IntegrityMet	TestFormal_IntegrityLevelOrder	Integrity ordinal order enforced; content below threshold denied with -32006
P6_IntegrityMet (unknown content)	TestFormal_UnknownContentIntegrityDenied	Unknown ContentIntegrity value (rank -1) denied as below any threshold
P6_IntegrityMet (invalid config)	TestFormal_InvalidMinIntegrityConfigDenied	Unrecognized MinIntegrity config is fail-safe: denies all requests
INV1_CombinedAllow	TestFormal_CombinedFiltersAllAllow	All six guards must be satisfied jointly for an allow decision
INV2_ErrorCode	TestFormal_ErrorCodeFirstFailingGuard	Deny error code matches first failing guard; table covers each guard as first failure
SAFETY_BlockedUserAlwaysDenied	TestFormal_BlockedUserSafetyProperty	Safety: blocked user always produces -32005 when all earlier guards pass
SAFETY_NoSpuriousAllow	TestFormal_NoSpuriousAllowInvariant	Safety: no allow decision when any guard fails
P5+P6 (evaluation order)	TestFormal_FixtureRunner	P5 fires before P6; fixture runner validates all YAML compliance scenarios

Generated Test Suite

📄 `pkg/workflow/github_mcp_access_control_formal_test.go`

(go/redacted):build !integration

package workflow

import (
	"os"
	"path/filepath"
	"slices"
	"strings"
	"testing"

	"github.com/stretchr/testify/assert"
	"github.com/stretchr/testify/require"
	yamlv3 "gopkg.in/yaml.v3"
)

// Specification: specs/github-mcp-access-control-compliance/README.md
// Formal predicates encoded by this file:
//   P1_ToolAllowed       — allowed-tools filter (spec §4.3)
//   P2_RepoMatch         — repos scope filter with pattern matching (spec §4.4.1)
//   P3_RoleAllow         — roles authorization (spec §4.4.2)
//   P4_PrivateRepoAllow  — private-repos visibility gate (spec §4.4.3)
//   P5_NotBlocked        — blocked-users integrity guard (spec §4.5.1)
//   P6_IntegrityMet      — min-integrity threshold (spec §4.5.2)
//   INV1_CombinedAllow   — all guards must hold for allow
//   INV2_ErrorCode       — first failing guard determines error code
//   SAFETY_BlockedUser   — blocked user always denied with -32005
//   SAFETY_NoSpurious    — no spurious allow when any guard fails

// Guard-policy error codes, aligned with pkg/cli/gateway_logs_types.go and the normative
// GitHub MCP access-control specification (Appendix B).
const (
	formalErrorToolNotAllowed    = -32001 // tool not in allowed-tools (general access denied)
	formalErrorRepoNotAllowed    = -32002 // repos guard failed
	formalErrorInsufficientRole  = -32003 // roles guard failed
	formalErrorPrivateRepoDenied = -32004 // private-repos: false guard failed
	formalErrorBlockedUser       = -32005 // blocked-users guard failed (within integrity management)
	formalErrorIntegrityTooLow   = -32006 // min-integrity guard failed
)

type formalToolConfig struct {
	Repos        []string
	Roles        []string
	PrivateRepos *bool
	AllowedTools []string
	BlockedUsers []string
	MinIntegrity string
}

type formalAccessRequest struct {
	Repository       string
	UserRole         string
	IsPrivate        bool
	ToolName         string
	UserLogin        string
	ContentIntegrity string
}

// TestFormal_ExactMatchAllow verifies P2_RepoMatch with exact owner/repo patterns.
func TestFormal_ExactMatchAllow(t *testing.T) {
	allowed := formalEvaluateAccess(formalToolConfig{Repos: []string{"github/gh-aw"}}, formalAccessRequest{Repository: "github/gh-aw"})
	denied := formalEvaluateAccess(formalToolConfig{Repos: []string{"github/gh-aw"}}, formalAccessRequest{Repository: "github/other"})

	assert.True(t, allowed.allow, "exact pattern should allow matching repo")
	assert.False(t, denied.allow, "exact pattern should deny non-matching repo")
	assert.Equal(t, formalErrorRepoNotAllowed, denied.errorCode, "repo mismatch must yield -32002")
}

// TestFormal_WildcardMatch verifies P2_RepoMatch with wildcard patterns.
func TestFormal_WildcardMatch(t *testing.T) {
	assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"github/*"}}, formalAccessRequest{Repository: "github/gh-aw"}).allow, "owner/* should allow same-owner repo")
	assert.False(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"github/*"}}, formalAccessRequest{Repository: "microsoft/vscode"}).allow, "owner/* should deny different-owner repo")
	assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/gh-aw"}}, formalAccessRequest{Repository: "github/gh-aw"}).allow, "*/repo should allow any-owner match")
	assert.False(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/gh-aw"}}, formalAccessRequest{Repository: "github/other"}).allow, "*/repo should deny non-matching name")
	assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/*"}}, formalAccessRequest{Repository: "any/repo"}).allow, "*/* should allow any repo")
}

// TestFormal_OmittedReposAllowAll verifies P2_RepoMatch: nil repos = no restriction.
func TestFormal_OmittedReposAllowAll(t *testing.T) {
	assert.True(t, formalEvaluateAccess(formalToolConfig{}, formalAccessRequest{Repository: "github/gh-aw"}).allow, "omitted repos must allow any repo")
	assert.True(t, formalEvaluateAccess(formalToolConfig{}, formalAccessRequest{Repository: "microsoft/vscode"}).allow, "omitted repos must allow any repo")
	assert.False(t, formalEvaluateAccess(formalToolConfig{Repos: []string{}}, formalAccessRequest{Repository: "github/gh-aw"}).allow, "empty repos slice must deny (invalid config)")
}

// TestFormal_RoleFilter verifies P3_RoleAllow with OR-logic over configured roles.
func TestFormal_RoleFilter(t *testing.T) {
	cfg := formalToolConfig{Repos: []string{"*/*"}, Roles: []string{"write", "admin"}}
	assert.True(t, formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", UserRole: "write"}).allow, "write role should be allowed")
	denied := formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", UserRole: "read"})
	assert.False(t, denied.allow, "read role should be denied when not in roles list")
	assert.Equal(t, formalErrorInsufficientRole, denied.errorCode, "role mismatch must yield -32003")
}

// TestFormal_PrivateRepoControl verifies P4_PrivateRepoAllow.
func TestFormal_PrivateRepoControl(t *testing.T) {
	allowPrivate := true
	denyPrivate := false
	assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"myorg/*"}, PrivateRepos: &allowPrivate}, formalAccessRequest{Repository: "myorg/private", IsPrivate: true}).allow, "private-repos:true allows private repos")
	assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"myorg/*"}, PrivateRepos: &denyPrivate}, formalAccessRequest{Repository: "myorg/public", IsPrivate: false}).allow, "private-repos:false still allows public repos")
	denied := formalEvaluateAccess(formalToolConfig{Repos: []string{"myorg/*"}, PrivateRepos: &denyPrivate}, formalAccessRequest{Repository: "myorg/private", IsPrivate: true})
	assert.False(t, denied.allow, "private-repos:false must deny private repos")
	assert.Equal(t, formalErrorPrivateRepoDenied, denied.errorCode, "private repo block must yield -32004")
}

// TestFormal_BlockedUserDeny verifies P5_NotBlocked within integrity management.
func TestFormal_BlockedUserDeny(t *testing.T) {
	cfg := formalToolConfig{Repos: []string{"github/gh-aw"}, Roles: []string{"write"}, BlockedUsers: []string{"bad-actor"}}
	assert.True(t, formalEvaluateAccess(cfg, formalAccessRequest{
		Repository: "github/gh-aw", UserRole: "write", UserLogin: "good-actor", ContentIntegrity: "approved",
	}).allow, "non-blocked user should be allowed")
	denied := formalEvaluateAccess(cfg, formalAccessRequest{
		Repository: "github/gh-aw", UserRole: "write", UserLogin: "bad-actor", ContentIntegrity: "approved",
	})
	assert.False(t, denied.allow, "blocked user must be denied")
	assert.Equal(t, formalErrorBlockedUser, denied.errorCode, "blocked user must yield -32005")
}

// TestFormal_ToolNameFilter verifies P1_ToolAllowed.
func TestFormal_ToolNameFilter(t *testing.T) {
	cfg := formalToolConfig{Repos: []string{"*/*"}, AllowedTools: []string{"issue_read"}}
	assert.True(t, formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", ToolName: "issue_read"}).allow, "listed tool should be allowed")
	assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/*"}}, formalAccessRequest{Repository: "github/gh-aw", ToolName: "delete_repo"}).allow, "no allowed-tools config = any tool allowed")
	denied := formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", ToolName: "delete_repo"})
	assert.False(t, denied.allow, "tool not in allowlist must be denied")
	assert.Equal(t, formalErrorToolNotAllowed, denied.errorCode, "tool not allowed must yield -32001")
	deniedEmpty := formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", ToolName: ""})
	assert.False(t, deniedEmpty.allow, "empty tool name against non-empty allowlist must be denied")
	assert.Equal(t, formalErrorToolNotAllowed, deniedEmpty.errorCode, "empty tool name must yield -32001")
}

// TestFormal_IntegrityLevelOrder verifies P6_IntegrityMet ordinal ordering.
func TestFormal_IntegrityLevelOrder(t *testing.T) {
	cases := []struct {
		name     string
		content  string
		min      string
		allowed  bool
	}{
		{"approved meets approved threshold", "approved", "approved", true},
		{"merged exceeds approved threshold", "merged", "approved", true},
		{"unapproved below approved threshold", "unapproved", "approved", false},
		{"none below unapproved threshold", "none", "unapproved", false},
		{"merged meets merged threshold", "merged", "merged", true},
	}
	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			res := formalEvaluateAccess(
				formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: tc.min},
				formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: tc.content},
			)
			if tc.allowed {
				assert.True(t, res.allow, "%s: expected allow", tc.name)
			} else {
				assert.False(t, res.allow, "%s: expected deny", tc.name)
				assert.Equal(t, formalErrorIntegrityTooLow, res.errorCode, "%s: must yield -32006", tc.name)
			}
		})
	}
}

// TestFormal_UnknownContentIntegrityDenied verifies P6 edge case: unknown rank = -1.
func TestFormal_UnknownContentIntegrityDenied(t *testing.T) {
	denied := formalEvaluateAccess(
		formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: "approved"},
		formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "unknown-level"},
	)
	assert.False(t, denied.allow, "unknown content integrity must be denied")
	assert.Equal(t, formalErrorIntegrityTooLow, denied.errorCode, "unknown content must yield -32006")
}

// TestFormal_InvalidMinIntegrityConfigDenied verifies P6 fail-safe: bad config denies all.
func TestFormal_InvalidMinIntegrityConfigDenied(t *testing.T) {
	denied := formalEvaluateAccess(
		formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: "invalid"},
		formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "merged"},
	)
	assert.False(t, denied.allow, "invalid min-integrity config must fail-safe deny")
	assert.Equal(t, formalErrorIntegrityTooLow, denied.errorCode, "invalid config must yield -32006")
}

// TestFormal_CombinedFiltersAllAllow verifies INV1: all six guards must hold jointly.
func TestFormal_CombinedFiltersAllAllow(t *testing.T) {
	allowPrivate := true
	cfg := formalToolConfig{
		Repos:        []string{"github/gh-aw"},
		Roles:        []string{"write"},
		PrivateRepos: &allowPrivate,
		AllowedTools: []string{"issue_read"},
		MinIntegrity: "approved",
	}
	assert.True(t, formalEvaluateAccess(cfg, formalAccessRequest{
		Repository: "github/gh-aw", UserRole: "write", IsPrivate: true, ToolName: "issue_read", UserLogin: "good-user", ContentIntegrity: "approved",
	}).allow, "all guards passing must produce allow")
}

// TestFormal_ErrorCodeFirstFailingGuard verifies INV2: first failing guard sets error code.
func TestFormal_ErrorCodeFirstFailingGuard(t *testing.T) {
	denyPrivate := false
	cfg := formalToolConfig{
		Repos:        []string{"github/gh-aw"},
		Roles:        []string{"write"},
		PrivateRepos: &denyPrivate,
		AllowedTools: []string{"issue_read"},
		BlockedUsers: []string{"bad-actor"},
		MinIntegrity: "approved",
	}
	cases := []struct {
		name     string
		req      formalAccessRequest
		wantCode int
	}{
		{"tool fails first", formalAccessRequest{Repository: "github/other", UserRole: "read", IsPrivate: true, ToolName: "delete_repo", UserLogin: "bad-actor", ContentIntegrity: "none"}, formalErrorToolNotAllowed},
		{"repo fails first", formalAccessRequest{Repository: "github/other", UserRole: "read", IsPrivate: true, ToolName: "issue_read", UserLogin: "bad-actor", ContentIntegrity: "none"}, formalErrorRepoNotAllowed},
		{"role fails first", formalAccessRequest{Repository: "github/gh-aw", UserRole: "read", IsPrivate: true, ToolName: "issue_read", UserLogin: "bad-actor", ContentIntegrity: "none"}, formalErrorInsufficientRole},
		{"private-repo fails first", formalAccessRequest{Repository: "github/gh-aw", UserRole: "write", IsPrivate: true, ToolName: "issue_read", UserLogin: "bad-actor", ContentIntegrity: "none"}, formalErrorPrivateRepoDenied},
		{"blocked-user fails first", formalAccessRequest{Repository: "github/gh-aw", UserRole: "write", IsPrivate: false, ToolName: "issue_read", UserLogin: "bad-actor", ContentIntegrity: "none"}, formalErrorBlockedUser},
		{"integrity fails first", formalAccessRequest{Repository: "github/gh-aw", UserRole: "write", IsPrivate: false, ToolName: "issue_read", UserLogin: "good-actor", ContentIntegrity: "none"}, formalErrorIntegrityTooLow},
	}
	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			d := formalEvaluateAccess(cfg, tc.req)
			assert.False(t, d.allow, "%s: must be denied", tc.name)
			assert.Equal(t, tc.wantCode, d.errorCode, "%s: wrong error code", tc.name)
		})
	}
}

// TestFormal_BlockedUserSafetyProperty verifies SAFETY_BlockedUserAlwaysDenied.
func TestFormal_BlockedUserSafetyProperty(t *testing.T) {
	allowPrivate := true
	cfg := formalToolConfig{
		Repos: []string{"*/*"}, Roles: []string{"admin"}, PrivateRepos: &allowPrivate,
		AllowedTools: []string{"issue_read"}, BlockedUsers: []string{"blocked"}, MinIntegrity: "merged",
	}
	denied := formalEvaluateAccess(cfg, formalAccessRequest{
		Repository: "any/repo", UserRole: "admin", IsPrivate: false,
		ToolName: "issue_read", UserLogin: "blocked", ContentIntegrity: "merged",
	})
	assert.False(t, denied.allow, "blocked user must always be denied")
	assert.Equal(t, formalErrorBlockedUser, denied.errorCode, "blocked user must yield -32005")
}

// TestFormal_NoSpuriousAllowInvariant verifies SAFETY_NoSpuriousAllow.
func TestFormal_NoSpuriousAllowInvariant(t *testing.T) {
	allowPrivate := true
	cfg := formalToolConfig{
		Repos: []string{"github/gh-aw"}, Roles: []string{"write"}, PrivateRepos: &allowPrivate,
		AllowedTools: []string{"issue_read"}, BlockedUsers: []string{"blocked"}, MinIntegrity: "approved",
	}
	cases := []formalAccessRequest{
		{Repository: "github/other", UserRole: "write", ToolName: "issue_read", ContentIntegrity: "approved"},
		{Repository: "github/gh-aw", UserRole: "read", ToolName: "issue_read", ContentIntegrity: "approved"},
		{Repository: "github/gh-aw", UserRole: "write", ToolName: "delete_repo", ContentIntegrity: "approved"},
		{Repository: "github/gh-aw", UserRole: "write", ToolName: "issue_read", ContentIntegrity: "none"},
		{Repository: "github/gh-aw", UserRole: "write", UserLogin: "blocked", ToolName: "issue_read", ContentIntegrity: "approved"},
	}
	for i, req := range cases {
		assert.False(t, formalEvaluateAccess(cfg, req).allow, "case %d must not be spuriously allowed", i)
	}
}

type formalDecision struct {
	allow     bool
	errorCode int
}

func formalEvaluateAccess(cfg formalToolConfig, req formalAccessRequest) formalDecision {
	// Guard evaluation order (spec §4.5.3): tool → repo → role → private-repo → blocked-user → integrity
	if len(cfg.AllowedTools) > 0 && !containsExact(cfg.AllowedTools, req.ToolName) {
		return formalDecision{errorCode: formalErrorToolNotAllowed}
	}
	if !formalRepositoryAllowed(cfg.Repos, req.Repository) {
		return formalDecision{errorCode: formalErrorRepoNotAllowed}
	}
	if len(cfg.Roles) > 0 && !containsExact(cfg.Roles, req.UserRole) {
		return formalDecision{errorCode: formalErrorInsufficientRole}
	}
	if cfg.PrivateRepos != nil && !*cfg.PrivateRepos && req.IsPrivate {
		return formalDecision{errorCode: formalErrorPrivateRepoDenied}
	}
	if containsExact(cfg.BlockedUsers, req.UserLogin) {
		return formalDecision{errorCode: formalErrorBlockedUser}
	}
	if cfg.MinIntegrity != "" {
		cfgRank := formalIntegrityRank(cfg.MinIntegrity)
		reqRank := formalIntegrityRank(req.ContentIntegrity)
		if cfgRank < 0 {
			return formalDecision{errorCode: formalErrorIntegrityTooLow}
		}
		if reqRank < cfgRank {
			return formalDecision{errorCode: formalErrorIntegrityTooLow}
		}
	}
	return formalDecision{allow: true}
}

func formalRepositoryAllowed(patterns []string, repository string) bool {
	if patterns == nil {
		return true
	}
	if len(patterns) == 0 {
		return false
	}
	repoOwner, repoName, ok := strings.Cut(repository, "/")
	if !ok || repoOwner == "" || repoName == "" {
		return false
	}
	for _, pattern := range patterns {
		patternOwner, patternRepo, ok := strings.Cut(pattern, "/")
		if !ok {
			continue
		}
		switch {
		case patternOwner == "*" && patternRepo == "*":
			return true
		case patternOwner == "*" && patternRepo == repoName:
			return true
		case patternOwner == repoOwner && patternRepo == "*":
			return true
		case patternOwner == repoOwner && patternRepo == repoName:
			return true
		}
	}
	return false
}

func formalIntegrityRank(level string) int {
	switch strings.ToLower(level) {
	case "none":
		return 0
	case "unapproved":
		return 1
	case "approved":
		return 2
	case "merged":
		return 3
	default:
		return -1
	}
}

func containsExact(values []string, needle string) bool {
	return slices.Contains(values, needle)
}

// ---------------------------------------------------------------------------
// Compliance fixture runner
// ---------------------------------------------------------------------------

type fixtureFile struct {
	FixtureID   string            `yaml:"fixture_id"`
	Description string            `yaml:"description"`
	Scenarios   []fixtureScenario `yaml:"scenarios"`
}

type fixtureScenario struct {
	ScenarioID  string          `yaml:"scenario_id"`
	Description string          `yaml:"description"`
	Input       fixtureInput    `yaml:"input"`
	Expected    fixtureExpected `yaml:"expected"`
}

type fixtureInput struct {
	ToolConfig fixtureToolConfig `yaml:"tool_config"`
	Request    fixtureRequest    `yaml:"request"`
}

type fixtureToolConfig struct {
	Repos        []string `yaml:"repos"`
	Roles        []string `yaml:"roles"`
	PrivateRepos *bool    `yaml:"private-repos"`
	AllowedTools []string `yaml:"allowed-tools"`
	BlockedUsers []string `yaml:"blocked-users"`
	MinIntegrity string   `yaml:"min-integrity"`
}

type fixtureRequest struct {
	Repository       string `yaml:"repository"`
	UserRole         string `yaml:"user_role"`
	IsPrivate        bool   `yaml:"is_private"`
	ToolName         string `yaml:"tool_name"`
	UserLogin        string `yaml:"user_login"`
	ContentIntegrity string `yaml:"content_integrity"`
}

type fixtureExpected struct {
	Decision  string `yaml:"decision"`
	ErrorCode *int   `yaml:"error_code"`
	Reason    string `yaml:"reason"`
}

// TestFormal_FixtureRunner drives every YAML compliance fixture through formalEvaluateAccess.
func TestFormal_FixtureRunner(t *testing.T) {
	fixtureDir := filepath.Join("..", "..", "specs", "github-mcp-access-control-compliance")
	entries, err := os.ReadDir(fixtureDir)
	require.NoError(t, err, "failed to read compliance fixture directory")

	var totalScenarios int
	for _, entry := range entries {
		if entry.IsDir() || filepath.Ext(entry.Name()) != ".yaml" {
			continue
		}
		fixturePath := filepath.Join(fixtureDir, entry.Name())
		data, err := os.ReadFile(fixturePath)
		require.NoErrorf(t, err, "failed to read fixture file %s", entry.Name())

		var ff fixtureFile
		require.NoErrorf(t, yamlv3.Unmarshal(data, &ff), "failed to parse fixture file %s", entry.Name())

		for _, sc := range ff.Scenarios {
			totalScenarios++
			t.Run(sc.ScenarioID, func(t *testing.T) {
				cfg := formalToolConfig{
					Repos: sc.Input.ToolConfig.Repos, Roles: sc.Input.ToolConfig.Roles,
					PrivateRepos: sc.Input.ToolConfig.PrivateRepos, AllowedTools: sc.Input.ToolConfig.AllowedTools,
					BlockedUsers: sc.Input.ToolConfig.BlockedUsers, MinIntegrity: sc.Input.ToolConfig.MinIntegrity,
				}
				req := formalAccessRequest{
					Repository: sc.Input.Request.Repository, UserRole: sc.Input.Request.UserRole,
					IsPrivate: sc.Input.Request.IsPrivate, ToolName: sc.Input.Request.ToolName,
					UserLogin: sc.Input.Request.UserLogin, ContentIntegrity: sc.Input.Request.ContentIntegrity,
				}
				got := formalEvaluateAccess(cfg, req)
				if sc.Expected.Decision == "allow" {
					assert.True(t, got.allow, "%s: expected allow", sc.ScenarioID)
					assert.Zero(t, got.errorCode, "%s: allow must have zero error code", sc.ScenarioID)
				} else {
					assert.False(t, got.allow, "%s: expected deny", sc.ScenarioID)
					if sc.Expected.ErrorCode != nil {
						assert.Equal(t, *sc.Expected.ErrorCode, got.errorCode, "%s: wrong error code", sc.ScenarioID)
					}
				}
			})
		}
	}
	require.Positive(t, totalScenarios, "fixture runner must find at least one scenario")
}

Usage

1. Copy or verify the test file at pkg/workflow/github_mcp_access_control_formal_test.go.
2. No stub interfaces needed — all types and helpers are self-contained in the file.
3. Run predicate-mapped tests: go test -v -run 'TestFormal_' ./pkg/workflow/
4. Run only the fixture runner: go test -v -run 'TestFormal_FixtureRunner' ./pkg/workflow/

Context

• Spec processed: specs/github-mcp-access-control-compliance/README.md
• Formal notation: Z3 / SMT-LIB + TLA+ (illustrative, not compiled)
• Predicates formalized: 10 (P1–P6, INV1, INV2, SAFETY×2)
• Test functions generated: 15
• Run: https://github.com/github/gh-aw/actions/runs/30023187661

Generated by 🔬 Daily Formal Spec Verifier · sonnet46 · 110.4 AIC · ⌖ 12.8 AIC · ⊞ 7.2K · ◷

• expires on Jul 30, 2026, 8:13 AM UTC-08:00