feat(formal-spec): add PRECOND_BlockedUsersRequireMinIntegrity to access-control formal model

pkg/workflow/github_mcp_access_control_formal_test.go

@@ -3,6 +3,7 @@
 package workflow
 
 import (
+	"errors"
 	"os"
 	"path/filepath"
 	"slices"
@@ -268,6 +269,31 @@ func TestFormal_BlockedUserSafetyProperty(t *testing.T) {
 	assert.Equal(t, formalErrorBlockedUser, denied.errorCode)
 }
 
+func TestFormal_BlockedUsersRequireMinIntegrity(t *testing.T) {
+	// PRECOND_BlockedUsersRequireMinIntegrity: a configuration that sets blocked-users
+	// without min-integrity is invalid and must be rejected at validation time.
+	err := formalValidateConfig(formalToolConfig{
+		Repos:        []string{"*/*"},
+		BlockedUsers: []string{"bad-actor"},
+		MinIntegrity: "",
+	})
+	require.Error(t, err, "blocked-users without min-integrity must be a validation error")
+
+	// With min-integrity set, the configuration is valid.
+	assert.NoError(t, formalValidateConfig(formalToolConfig{
+		Repos:        []string{"*/*"},
+		BlockedUsers: []string{"bad-actor"},
+		MinIntegrity: "approved",
+	}))
+
+	// An empty blocked-users list without min-integrity is valid (no guard active).
+	assert.NoError(t, formalValidateConfig(formalToolConfig{
+		Repos:        []string{"*/*"},
+		BlockedUsers: nil,
+		MinIntegrity: "",
+	}))
+}
+
 func TestFormal_NoSpuriousAllowInvariant(t *testing.T) {
 	allowPrivate := true
 	cfg := formalToolConfig{
@@ -297,6 +323,16 @@ type formalDecision struct {
 	errorCode int
 }
 
+// formalValidateConfig mirrors the compile-time validation preconditions for
+// formalToolConfig. It enforces PRECOND_BlockedUsersRequireMinIntegrity: blocked-users
+// requires min-integrity to be set.
+func formalValidateConfig(cfg formalToolConfig) error {
+	if len(cfg.BlockedUsers) > 0 && cfg.MinIntegrity == "" {
+		return errors.New("invalid guard policy: blocked-users requires min-integrity to be set")
+	}
+	return nil
+}
+
 func formalEvaluateAccess(cfg formalToolConfig, req formalAccessRequest) formalDecision {
 	// Guard evaluation order (spec §4.5.3):
 	// 1. Tool selection (allowed-tools)

specs/github-mcp-access-control-compliance/README.md

@@ -62,6 +62,7 @@ The denial code is selected by the first failing guard in the evaluation order a
 | `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 |
+| `PRECOND_BlockedUsersRequireMinIntegrity` | `TestFormal_BlockedUsersRequireMinIntegrity` | Validation error when blocked-users set without min-integrity |
 
 ## Fixture Files