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

[github-actions]

Summary

The GitHub MCP Access Control Compliance Fixtures specification defines nine structured test scenarios that capture the normative access-control requirements (§§4–10) of the GitHub MCP Server Access Control Specification. This formalization models the six orthogonal access-control dimensions — repository allowlist matching, role-based filtering, private-repository controls, tool-name filtering, blocked-user enforcement, and content integrity level enforcement — as a conjunction of guard predicates over an AccessRequest × ToolConfig → Decision function. The formal model expresses each predicate in TLA+/Z3-style notation and maps each directly to a Go testify test function.

Specification

• File: specs/github-mcp-access-control-compliance/README.md
• Focus area: MCP Gateway runtime access-control decision engine
• Formal notation used: TLA+ (state-transition guards), Z3 / SMT-LIB (arithmetic ordering for integrity levels)

Formal Model

Predicates and invariants (illustrative notation)

(* ──────────────────────────────────────────────────────────
   Formal Model: GitHub MCP Access Control
   Source: specs/github-mcp-access-control-compliance/README.md
   §§4–10 of the GitHub MCP Server Access Control Specification
   ────────────────────────────────────────────────────────── *)

(* Types *)
REPO      == STRING  (* "owner/name" *)
ROLE      == { "read", "triage", "write", "maintain", "admin", "" }
INTEG     == { "none", "unapproved", "approved", "merged" }
DECISION  == { "allow", "deny" }
ERR_CODE  == { -32001, -32002, -32003, -32004, -32005, -32006, null }

IntegOrd(l) == CASE l = "none"       -> 0
             []  l = "unapproved"   -> 1
             []  l = "approved"     -> 2
             []  l = "merged"       -> 3

(* P1 — Exact-pattern repository match §5.1
   Source: exact-match-allow fixture, scenarios A & B *)
P1_ExactMatch(repos, req_repo) ==
  \E p \in repos : p = req_repo

(* P2 — Wildcard-pattern repository match §5.2
   Source: wildcard-deny fixture *)
P2_WildcardMatch(repos, req_repo) ==
  LET owner == Head(Split(req_repo, "/"))
      name  == Last(Split(req_repo, "/"))
  IN  \E p \in repos :
        \/ p = req_repo
        \/ p = owner ++ "/*"
        \/ (StartsWith(p, owner ++ "/") /\ EndsWith(p, "*") /\
             StartsWith(name, SubStr(p, Len(owner)+2, Len(p)-Len(owner)-2)))
        \/ p = "*/*"

(* P3 — Empty / absent repos list denies all §5.3
   Source: empty-repos-block fixture *)
P3_EmptyReposDenyAll(repos) ==
  repos = {} \/ repos = <<>>

(* Combined repository guard *)
RepoAllow(cfg, req) ==
  ~P3_EmptyReposDenyAll(cfg.repos) /\ P2_WildcardMatch(cfg.repos, req.repository)

(* P4 — Role filter §6 (role-deny fixture)
   OR-logic over configured roles *)
P4_RoleAllow(cfg, req) ==
  cfg.roles = {} \/ req.user_role \in cfg.roles

(* P5 — Private repository control §7
   Source: private-repo-block fixture *)
P5_PrivateRepoAllow(cfg, req) ==
  \/ cfg.private_repos = true
  \/ req.is_private = false

(* P6 — Blocked-user unconditional deny §7.2
   Source: blocked-user-deny fixture *)
P6_NotBlocked(cfg, req) ==
  req.user_login \notin cfg.blocked_users

(* P7 — Allowed-tools filter §6.1
   Source: tool-name-filter fixture *)
P7_ToolAllowed(cfg, req) ==
  cfg.allowed_tools = {} \/ req.tool_name \in cfg.allowed_tools

(* P8 — Integrity level threshold §8 (Z3 ordinal)
   Source: integrity-level-block fixture
   Constraint: IntegOrd(req.content_integrity) >= IntegOrd(cfg.min_integrity) *)
P8_IntegrityMet(cfg, req) ==
  cfg.min_integrity = "" \/ IntegOrd(req.content_integrity) >= IntegOrd(cfg.min_integrity)

(* INV1 — Conjunction: all guards must pass for allow (combined-filter-allow)
   Source: §10.1-10.3 *)
INV1_CombinedAllow(cfg, req) ==
  /\ RepoAllow(cfg, req)
  /\ P4_RoleAllow(cfg, req)
  /\ P5_PrivateRepoAllow(cfg, req)
  /\ P6_NotBlocked(cfg, req)
  /\ P7_ToolAllowed(cfg, req)
  /\ P8_IntegrityMet(cfg, req)

(* INV2 — Error code assignment §10.3 (first-failing guard in evaluation order) *)
INV2_ErrorCode(cfg, req) ==
  IF   ~RepoAllow(cfg, req)         THEN -32001
  ELSE IF ~P4_RoleAllow(cfg, req)   THEN -32002
  ELSE IF ~P5_PrivateRepoAllow(cfg, req) THEN -32003
  ELSE IF ~P6_NotBlocked(cfg, req)  THEN -32004
  ELSE IF ~P7_ToolAllowed(cfg, req) THEN -32005
  ELSE IF ~P8_IntegrityMet(cfg, req) THEN -32006
  ELSE null

(* SAFETY — No request is allowed when any guard fails *)
SAFETY_NoSpuriousAllow ==
  \A cfg, req : Decide(cfg, req) = "allow" => INV1_CombinedAllow(cfg, req)

(* SAFETY — Blocked user is always denied regardless of other conditions *)
SAFETY_BlockedUserAlwaysDenied ==
  \A cfg, req : req.user_login \in cfg.blocked_users =>
    Decide(cfg, req) = "deny" /\ INV2_ErrorCode(cfg, req) = -32004

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
P1_ExactMatch	TestFormal_ExactMatchAllow	Exact owner/repo pattern allows matching repo, denies others
P2_WildcardMatch	TestFormal_WildcardMatch	Owner-wildcard owner/* and prefix-wildcard owner/prefix-* matching
P3_EmptyReposDenyAll	TestFormal_EmptyReposDenyAll	Absent or empty repos list denies every repository
P4_RoleAllow	TestFormal_RoleFilter	Role OR-logic: matching role allows, insufficient role denies
P5_PrivateRepoAllow	TestFormal_PrivateRepoControl	private-repos: false blocks private repos; public repos unaffected
P6_NotBlocked	TestFormal_BlockedUserDeny	Blocked user denied unconditionally regardless of other conditions
P7_ToolAllowed	TestFormal_ToolNameFilter	allowed-tools restricts callable tools; absent allows all
P8_IntegrityMet	TestFormal_IntegrityLevelOrder	Integrity ordinal order enforced; content below threshold denied
INV1_CombinedAllow	TestFormal_CombinedFiltersAllAllow	All conditions must be satisfied for allow
INV2_ErrorCode	TestFormal_ErrorCodeFirstFailingGuard	Deny error code matches first failing guard in evaluation order
SAFETY_BlockedUserAlwaysDenied	TestFormal_BlockedUserSafetyProperty	Safety: blocked user always produces -32004
SAFETY_NoSpuriousAllow	TestFormal_NoSpuriousAllowInvariant	Safety: no allow decision when any guard fails

Generated Test Suite

📄 `pkg/workflow/github_mcp_access_control_formal_test.go`

// github_mcp_access_control_formal_test.go
//
// Formal specification test suite for the GitHub MCP Access Control guard predicates.
//
// Specification file: specs/github-mcp-access-control-compliance/README.md
// Primary spec:       scratchpad/github-mcp-access-control-specification.md §§4–10
//
// Formal predicates encoded by this suite:
//   P1  ExactMatch       — §5.1  exact repository pattern allows / denies
//   P2  WildcardMatch    — §5.2  owner-wildcard and prefix-wildcard matching
//   P3  EmptyReposDenyAll— §5.3  absent or empty repos list denies all
//   P4  RoleAllow        — §6    OR-logic role filter
//   P5  PrivateRepoAllow — §7    private-repos flag
//   P6  NotBlocked       — §7.2  blocked-users unconditional deny
//   P7  ToolAllowed      — §6.1  allowed-tools filter
//   P8  IntegrityMet     — §8    min-integrity ordinal comparison
//   INV1 CombinedAllow   — §10   conjunction of all guards
//   INV2 ErrorCode       — §10.3 first-failing guard determines error code
//   SAFETY NoSpuriousAllow      — no allow when any guard fails
//   SAFETY BlockedUserAlwaysDenied — blocked user always -32004

(go/redacted):build !integration

package workflow_test

import (
	"testing"

	"github.com/stretchr/testify/assert"
	"github.com/stretchr/testify/require"
)

// ─────────────────────────────────────────────
// stub — replace with real implementation
// ─────────────────────────────────────────────

// MCPAccessRequest represents an incoming MCP tool invocation request.
type MCPAccessRequest struct {
	Repository       string
	UserLogin        string
	UserRole         string
	IsPrivate        bool
	ToolName         string
	ContentIntegrity string
}

// MCPToolConfig represents a compiled GitHub MCP tool access-control configuration.
type MCPToolConfig struct {
	Repos        []string
	Roles        []string
	PrivateRepos *bool // nil means "not set" (defaults to true)
	AllowedTools []string
	BlockedUsers []string
	MinIntegrity string
}

// MCPAccessDecision is the outcome of evaluating a request against a config.
type MCPAccessDecision struct {
	Allow     bool
	ErrorCode int // 0 when Allow is true
}

// integOrd returns the ordinal position of an integrity level.
func integOrd(level string) int {
	switch level {
	case "none":
		return 0
	case "unapproved":
		return 1
	case "approved":
		return 2
	case "merged":
		return 3
	}
	return -1
}

// repoMatchesPattern returns true when the repository string matches the given
// allowlist pattern. Supported patterns:
//   - "owner/repo"   — exact match
//   - "owner/*"      — all repos under the owner
//   - "owner/pfx-*" — repos whose name starts with pfx-
//   - "*/*"          — all repos
func repoMatchesPattern(pattern, repo string) bool {
	if pattern == "*/*" {
		return true
	}
	if pattern == repo {
		return true
	}
	// Split pattern and repo on "/"
	splitAt := func(s string) (string, string) {
		for i, c := range s {
			if c == '/' {
				return s[:i], s[i+1:]
			}
		}
		return s, ""
	}
	patOwner, patName := splitAt(pattern)
	reqOwner, reqName := splitAt(repo)
	if patOwner != reqOwner {
		return false
	}
	if patName == "*" {
		return true
	}
	// prefix wildcard: "gh-*" matches names beginning with "gh-"
	if len(patName) > 0 && patName[len(patName)-1] == '*' {
		prefix := patName[:len(patName)-1]
		return len(reqName) >= len(prefix) && reqName[:len(prefix)] == prefix
	}
	return false
}

// repoAllowed returns true when the request repository matches at least one
// pattern in the allowlist (P1/P2) and the allowlist is non-empty (P3).
func repoAllowed(cfg MCPToolConfig, req MCPAccessRequest) bool {
	if len(cfg.Repos) == 0 {
		return false
	}
	for _, p := range cfg.Repos {
		if repoMatchesPattern(p, req.Repository) {
			return true
		}
	}
	return false
}

// roleAllowed returns true when no roles are configured (unrestricted) or when
// the request user role is in the configured role set (P4 OR-logic).
func roleAllowed(cfg MCPToolConfig, req MCPAccessRequest) bool {
	if len(cfg.Roles) == 0 {
		return true
	}
	for _, r := range cfg.Roles {
		if r == req.UserRole {
			return true
		}
	}
	return false
}

// privateRepoAllowed returns true when private repos are permitted or the repo
// is not private (P5).
func privateRepoAllowed(cfg MCPToolConfig, req MCPAccessRequest) bool {
	if cfg.PrivateRepos == nil || *cfg.PrivateRepos {
		return true
	}
	return !req.IsPrivate
}

// notBlocked returns true when the user is not in the blocked-users list (P6).
func notBlocked(cfg MCPToolConfig, req MCPAccessRequest) bool {
	for _, u := range cfg.BlockedUsers {
		if u == req.UserLogin {
			return false
		}
	}
	return true
}

// toolAllowed returns true when no allowed-tools are configured or the requested
// tool is in the allowed list (P7).
func toolAllowed(cfg MCPToolConfig, req MCPAccessRequest) bool {
	if len(cfg.AllowedTools) == 0 {
		return true
	}
	for _, t := range cfg.AllowedTools {
		if t == req.ToolName {
			return true
		}
	}
	return false
}

// integrityMet returns true when no min-integrity is set or the content
// integrity is at or above the configured threshold (P8).
func integrityMet(cfg MCPToolConfig, req MCPAccessRequest) bool {
	if cfg.MinIntegrity == "" {
		return true
	}
	return integOrd(req.ContentIntegrity) >= integOrd(cfg.MinIntegrity)
}

// evaluate implements INV1 + INV2: returns the combined access decision.
func evaluate(cfg MCPToolConfig, req MCPAccessRequest) MCPAccessDecision {
	if !repoAllowed(cfg, req) {
		return MCPAccessDecision{Allow: false, ErrorCode: -32001}
	}
	if !roleAllowed(cfg, req) {
		return MCPAccessDecision{Allow: false, ErrorCode: -32002}
	}
	if !privateRepoAllowed(cfg, req) {
		return MCPAccessDecision{Allow: false, ErrorCode: -32003}
	}
	if !notBlocked(cfg, req) {
		return MCPAccessDecision{Allow: false, ErrorCode: -32004}
	}
	if !toolAllowed(cfg, req) {
		return MCPAccessDecision{Allow: false, ErrorCode: -32005}
	}
	if !integrityMet(cfg, req) {
		return MCPAccessDecision{Allow: false, ErrorCode: -32006}
	}
	return MCPAccessDecision{Allow: true, ErrorCode: 0}
}

// boolPtr is a helper for *bool literals.
func boolPtr(b bool) *bool { return &b }

// ─────────────────────────────────────────────
// P1 — Exact match (§5.1)
// ─────────────────────────────────────────────

func TestFormal_ExactMatchAllow(t *testing.T) {
	t.Parallel()
	cfg := MCPToolConfig{
		Repos:        []string{"github/gh-aw"},
		PrivateRepos: boolPtr(true),
		MinIntegrity: "unapproved",
	}
	tests := []struct {
		name       string
		repo       string
		wantAllow  bool
		wantErrCode int
	}{
		{"T-GH-011: exact match allows", "github/gh-aw", true, 0},
		{"T-GH-012: non-matching repo denies with -32001", "github/other-repo", false, -32001},
		{"edge: empty repo string denies", "", false, -32001},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			req := MCPAccessRequest{
				Repository:       tt.repo,
				UserRole:         "write",
				IsPrivate:        true,
				ContentIntegrity: "unapproved",
			}
			dec := evaluate(cfg, req)
			assert.Equal(t, tt.wantAllow, dec.Allow, "P1 ExactMatch: decision mismatch for repo %q", tt.repo)
			assert.Equal(t, tt.wantErrCode, dec.ErrorCode, "P1 ExactMatch: error code mismatch for repo %q", tt.repo)
		})
	}
}

// ─────────────────────────────────────────────
// P2 — Wildcard match (§5.2)
// ─────────────────────────────────────────────

func TestFormal_WildcardMatch(t *testing.T) {
	t.Parallel()
	tests := []struct {
		name      string
		patterns  []string
		repo      string
		wantAllow bool
	}{
		{"T-GH-013: owner/* allows any repo under owner", []string{"github/*"}, "github/any-repo", true},
		{"T-GH-014: owner/* denies repo under different owner", []string{"github/*"}, "microsoft/vscode", false},
		{"prefix wildcard gh-* denies non-matching name", []string{"github/gh-*"}, "github/copilot", false},
		{"prefix wildcard gh-* allows matching name", []string{"github/gh-*"}, "github/gh-aw", true},
		{"*/* allows any repo", []string{"*/*"}, "anyowner/anyrepo", true},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			cfg := MCPToolConfig{Repos: tt.patterns}
			req := MCPAccessRequest{Repository: tt.repo, ContentIntegrity: "none"}
			dec := evaluate(cfg, req)
			assert.Equal(t, tt.wantAllow, dec.Allow, "P2 WildcardMatch: decision mismatch for pattern %v repo %q", tt.patterns, tt.repo)
		})
	}
}

// ─────────────────────────────────────────────
// P3 — Empty repos list denies all (§5.3)
// ─────────────────────────────────────────────

func TestFormal_EmptyReposDenyAll(t *testing.T) {
	t.Parallel()
	tests := []struct {
		name  string
		repos []string
	}{
		{"T-GH-015: absent repos field", nil},
		{"T-GH-016: empty repos slice", []string{}},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			cfg := MCPToolConfig{Repos: tt.repos}
			req := MCPAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "unapproved"}
			dec := evaluate(cfg, req)
			assert.False(t, dec.Allow, "P3 EmptyReposDenyAll: expected deny for repos=%v", tt.repos)
			assert.Equal(t, -32001, dec.ErrorCode, "P3 EmptyReposDenyAll: expected -32001 error code")
		})
	}
}

// ─────────────────────────────────────────────
// P4 — Role filter OR-logic (§6)
// ─────────────────────────────────────────────

func TestFormal_RoleFilter(t *testing.T) {
	t.Parallel()
	cfg := MCPToolConfig{
		Repos:        []string{"*/*"},
		Roles:        []string{"write", "admin"},
		MinIntegrity: "none",
	}
	tests := []struct {
		name        string
		userRole    string
		wantAllow   bool
		wantErrCode int
	}{
		{"T-GH-019: write role is allowed", "write", true, 0},
		{"T-GH-023: admin role is allowed (OR-logic)", "admin", true, 0},
		{"T-GH-020: read role is denied", "read", false, -32002},
		{"edge: empty user role is denied", "", false, -32002},
		{"edge: unknown role is denied", "superuser", false, -32002},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			req := MCPAccessRequest{
				Repository:       "example/repo",
				UserRole:         tt.userRole,
				ContentIntegrity: "none",
			}
			dec := evaluate(cfg, req)
			assert.Equal(t, tt.wantAllow, dec.Allow, "P4 RoleFilter: decision mismatch for role %q", tt.userRole)
			assert.Equal(t, tt.wantErrCode, dec.ErrorCode, "P4 RoleFilter: error code mismatch for role %q", tt.userRole)
		})
	}
}

// ─────────────────────────────────────────────
// P5 — Private repository control (§7)
// ─────────────────────────────────────────────

func TestFormal_PrivateRepoControl(t *testing.T) {
	t.Parallel()
	tests := []struct {
		name         string
		privateRepos *bool
		isPrivate    bool
		wantAllow    bool
		wantErrCode  int
	}{
		{"T-GH-024: private-repos true allows private repo", boolPtr(true), true, true, 0},
		{"T-GH-025: private-repos false denies private repo", boolPtr(false), true, false, -32003},
		{"T-GH-026: private-repos false allows public repo", boolPtr(false), false, true, 0},
		{"default (nil) allows private repo", nil, true, true, 0},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			cfg := MCPToolConfig{
				Repos:        []string{"myorg/*"},
				PrivateRepos: tt.privateRepos,
				MinIntegrity: "none",
			}
			req := MCPAccessRequest{
				Repository:       "myorg/internal-tool",
				IsPrivate:        tt.isPrivate,
				ContentIntegrity: "none",
			}
			dec := evaluate(cfg, req)
			assert.Equal(t, tt.wantAllow, dec.Allow, "P5 PrivateRepo: decision mismatch")
			assert.Equal(t, tt.wantErrCode, dec.ErrorCode, "P5 PrivateRepo: error code mismatch")
		})
	}
}

// ─────────────────────────────────────────────
// P6 — Blocked user unconditional deny (§7.2)
// ─────────────────────────────────────────────

func TestFormal_BlockedUserDeny(t *testing.T) {
	t.Parallel()
	cfg := MCPToolConfig{
		Repos:        []string{"github/gh-aw"},
		Roles:        []string{"write"},
		PrivateRepos: boolPtr(true),
		MinIntegrity: "unapproved",
		BlockedUsers: []string{"bad-actor"},
	}
	tests := []struct {
		name        string
		userLogin   string
		wantAllow   bool
		wantErrCode int
	}{
		{"T-GH-071: blocked user is denied despite matching all other conditions", "bad-actor", false, -32004},
		{"T-GH-072: non-blocked user is allowed when all conditions are met", "good-contributor", true, 0},
		{"edge: empty user login is not blocked", "", true, 0},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			req := MCPAccessRequest{
				Repository:       "github/gh-aw",
				UserLogin:        tt.userLogin,
				UserRole:         "write",
				IsPrivate:        true,
				ContentIntegrity: "unapproved",
			}
			dec := evaluate(cfg, req)
			assert.Equal(t, tt.wantAllow, dec.Allow, "P6 BlockedUser: decision mismatch for user %q", tt.userLogin)
			assert.Equal(t, tt.wantErrCode, dec.ErrorCode, "P6 BlockedUser: error code mismatch for user %q", tt.userLogin)
		})
	}
}

// ─────────────────────────────────────────────
// P7 — Tool name filter (§6.1)
// ─────────────────────────────────────────────

func TestFormal_ToolNameFilter(t *testing.T) {
	t.Parallel()
	tests := []struct {
		name         string
		allowedTools []string
		toolName     string
		wantAllow    bool
		wantErrCode  int
	}{
		{"T-GH-031: listed tool is allowed", []string{"issue_read", "list_issues"}, "issue_read", true, 0},
		{"T-GH-032: unlisted tool is denied", []string{"issue_read", "list_issues"}, "delete_repository", false, -32005},
		{"T-GH-033: absent allowed-tools permits any tool", nil, "delete_repository", true, 0},
		{"edge: empty allowed-tools permits any tool", []string{}, "any_tool", true, 0},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			cfg := MCPToolConfig{
				Repos:        []string{"*/*"},
				AllowedTools: tt.allowedTools,
				MinIntegrity: "unapproved",
			}
			req := MCPAccessRequest{
				Repository:       "example/repo",
				ToolName:         tt.toolName,
				ContentIntegrity: "unapproved",
			}
			dec := evaluate(cfg, req)
			assert.Equal(t, tt.wantAllow, dec.Allow, "P7 ToolNameFilter: decision mismatch for tool %q", tt.toolName)
			assert.Equal(t, tt.wantErrCode, dec.ErrorCode, "P7 ToolNameFilter: error code mismatch for tool %q", tt.toolName)
		})
	}
}

// ─────────────────────────────────────────────
// P8 — Integrity level order (§8)
// ─────────────────────────────────────────────

func TestFormal_IntegrityLevelOrder(t *testing.T) {
	t.Parallel()

	// Verify the ordinal ordering: none < unapproved < approved < merged
	levels := []string{"none", "unapproved", "approved", "merged"}
	for i := 0; i < len(levels)-1; i++ {
		require.Less(t, integOrd(levels[i]), integOrd(levels[i+1]),
			"P8 integrity ordinal: %q must be strictly less than %q", levels[i], levels[i+1])
	}

	tests := []struct {
		name             string
		minIntegrity     string
		contentIntegrity string
		wantAllow        bool
		wantErrCode      int
	}{
		{"T-GH-051: content at threshold is allowed", "approved", "approved", true, 0},
		{"T-GH-051b: content above threshold (merged) is allowed", "approved", "merged", true, 0},
		{"T-GH-052: content below threshold is denied", "approved", "unapproved", false, -32006},
		{"T-GH-054: content at lowest level denied when min=merged", "merged", "none", false, -32006},
		{"T-GH-059: no min-integrity permits any content level", "", "none", true, 0},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			cfg := MCPToolConfig{
				Repos:        []string{"*/*"},
				MinIntegrity: tt.minIntegrity,
			}
			req := MCPAccessRequest{
				Repository:       "example/repo",
				ContentIntegrity: tt.contentIntegrity,
			}
			dec := evaluate(cfg, req)
			assert.Equal(t, tt.wantAllow, dec.Allow, "P8 Integrity: mismatch for min=%q content=%q", tt.minIntegrity, tt.contentIntegrity)
			assert.Equal(t, tt.wantErrCode, dec.ErrorCode, "P8 Integrity: error code mismatch")
		})
	}
}

// ─────────────────────────────────────────────
// INV1 — Combined filters: all must pass (§10.1-10.2)
// ─────────────────────────────────────────────

func TestFormal_CombinedFiltersAllAllow(t *testing.T) {
	t.Parallel()
	baseCfg := MCPToolConfig{
		Repos:        []string{"github/gh-aw"},
		Roles:        []string{"write"},
		PrivateRepos: boolPtr(true),
		MinIntegrity: "approved",
	}
	baseReq := MCPAccessRequest{
		Repository:       "github/gh-aw",
		UserRole:         "write",
		IsPrivate:        true,
		ContentIntegrity: "approved",
	}

	// T-GH-081: all conditions satisfied → allow
	dec := evaluate(baseCfg, baseReq)
	assert.True(t, dec.Allow, "INV1: all conditions satisfied must produce allow")
	assert.Equal(t, 0, dec.ErrorCode, "INV1: allow must produce zero error code")

	// T-GH-082 variants: each single failing condition must produce deny
	brokenRepoReq := baseReq
	brokenRepoReq.Repository = "github/other-repo"
	dec = evaluate(baseCfg, brokenRepoReq)
	assert.False(t, dec.Allow, "INV1: failing repo condition must deny")

	brokenRoleReq := baseReq
	brokenRoleReq.UserRole = "read"
	dec = evaluate(baseCfg, brokenRoleReq)
	assert.False(t, dec.Allow, "INV1: failing role condition must deny")

	brokenIntegReq := baseReq
	brokenIntegReq.ContentIntegrity = "none"
	dec = evaluate(baseCfg, brokenIntegReq)
	assert.False(t, dec.Allow, "INV1: failing integrity condition must deny")
}

// ─────────────────────────────────────────────
// INV2 — Error code reflects first failing guard (§10.3)
// ─────────────────────────────────────────────

func TestFormal_ErrorCodeFirstFailingGuard(t *testing.T) {
	t.Parallel()
	cfg := MCPToolConfig{
		Repos:        []string{"github/gh-aw"},
		Roles:        []string{"write"},
		PrivateRepos: boolPtr(true),
		MinIntegrity: "approved",
	}
	// T-GH-083: evaluation order determines error code
	tests := []struct {
		name        string
		req         MCPAccessRequest
		wantErrCode int
	}{
		{
			"repo fails first → -32001",
			MCPAccessRequest{Repository: "github/other", UserRole: "read", IsPrivate: true, ContentIntegrity: "none"},
			-32001,
		},
		{
			"role fails after repo passes → -32002",
			MCPAccessRequest{Repository: "github/gh-aw", UserRole: "read", IsPrivate: true, ContentIntegrity: "none"},
			-32002,
		},
		{
			"integrity fails last → -32006",
			MCPAccessRequest{Repository: "github/gh-aw", UserRole: "write", IsPrivate: true, ContentIntegrity: "none"},
			-32006,
		},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			t.Parallel()
			dec := evaluate(cfg, tt.req)
			assert.False(t, dec.Allow, "INV2 ErrorCode: expected deny")
			assert.Equal(t, tt.wantErrCode, dec.ErrorCode, "INV2 ErrorCode: wrong error code for first-failing guard")
		})
	}
}

// ─────────────────────────────────────────────
// SAFETY — Blocked user always -32004
// ─────────────────────────────────────────────

func TestFormal_BlockedUserSafetyProperty(t *testing.T) {
	t.Parallel()
	// Regardless of repo, role, visibility, or integrity: blocked user → -32004
	cfg := MCPToolConfig{
		Repos:        []string{"*/*"},
		PrivateRepos: boolPtr(true),
		BlockedUsers: []string{"blocked-actor"},
		MinIntegrity: "none",
	}
	variants := []MCPAccessRequest{
		{Repository: "any/repo", UserLogin: "blocked-actor", UserRole: "admin", IsPrivate: true, ContentIntegrity: "merged"},
		{Repository: "other/repo", UserLogin: "blocked-actor", UserRole: "write", IsPrivate: false, ContentIntegrity: "approved"},
		{Repository: "x/y", UserLogin: "blocked-actor", UserRole: "", IsPrivate: false, ContentIntegrity: "none"},
	}
	for _, req := range variants {
		dec := evaluate(cfg, req)
		assert.False(t, dec.Allow, "SAFETY BlockedUser: blocked-actor must always be denied")
		assert.Equal(t, -32004, dec.ErrorCode, "SAFETY BlockedUser: error code must be -32004 for blocked actor")
	}
}

// ─────────────────────────────────────────────
// SAFETY — No spurious allow when any guard fails
// ─────────────────────────────────────────────

func TestFormal_NoSpuriousAllowInvariant(t *testing.T) {
	t.Parallel()
	cfg := MCPToolConfig{
		Repos:        []string{"github/gh-aw"},
		Roles:        []string{"write"},
		PrivateRepos: boolPtr(false),
		AllowedTools: []string{"issue_read"},
		BlockedUsers: []string{"spammer"},
		MinIntegrity: "approved",
	}
	// Each request below violates exactly one guard.
	denyCases := []MCPAccessRequest{
		{Repository: "github/wrong", UserRole: "write", IsPrivate: false, ToolName: "issue_read", ContentIntegrity: "approved"},
		{Repository: "github/gh-aw", UserRole: "read", IsPrivate: false, ToolName: "issue_read", ContentIntegrity: "approved"},
		{Repository: "github/gh-aw", UserRole: "write", IsPrivate: true, ToolName: "issue_read", ContentIntegrity: "approved"},
		{Repository: "github/gh-aw", UserLogin: "spammer", UserRole: "write", IsPrivate: false, ToolName: "issue_read", ContentIntegrity: "approved"},
		{Repository: "github/gh-aw", UserRole: "write", IsPrivate: false, ToolName: "delete_repo", ContentIntegrity: "approved"},
		{Repository: "github/gh-aw", UserRole: "write", IsPrivate: false, ToolName: "issue_read", ContentIntegrity: "unapproved"},
	}
	for i, req := range denyCases {
		dec := evaluate(cfg, req)
		assert.False(t, dec.Allow, "SAFETY NoSpuriousAllow: case %d must be denied when one guard fails", i)
		assert.NotEqual(t, 0, dec.ErrorCode, "SAFETY NoSpuriousAllow: deny must carry non-zero error code in case %d", i)
	}
}

Usage

1. Copy github_mcp_access_control_formal_test.go to pkg/workflow/.
2. Replace the // stub type and function definitions with the real GitHubToolConfig-based implementation once the access-control engine is production-ready.
3. Run: go test ./pkg/workflow/... -run Formal

Context

• Spec processed: specs/github-mcp-access-control-compliance/README.md
• Formal notation: TLA+ (guard predicates, safety properties), Z3/SMT-LIB (integrity ordinal ordering)
• Run: https://github.com/github/gh-aw/actions/runs/29106346453

Generated by 🔬 Daily Formal Spec Verifier · 219 AIC · ⌖ 13 AIC · ⊞ 7.2K · ◷

• expires on Jul 17, 2026, 8:28 AM UTC-08:00