Skip to content

[formal-spec] intent-attribution-agent-governance.md — Formal model & test suite — 2026-08-18 #53741

Description

@github-actions

Summary

specs/intent-attribution-agent-governance.md defines a deterministic intent-attribution and agent-governance layer for agentic GitHub workflows: it resolves why a PR/issue exists (intent), derives a risk classification, compiles a fail-closed ExecutionPolicy via precedence-ordered rules, and (per the spec's own audit note) still lacks a wired Authorizer.AuthorizeTool enforcement point. This formalization focuses on the Risk classification and Enforcement sections, since ResolveRisk and AuthorizeTool are specified but not yet implemented in pkg/intent, while PolicyCompiler.Compile's fail-closed behavior for indeterminate attribution is already implemented and cross-checked here.

Specification

  • File: specs/intent-attribution-agent-governance.md
  • Focus area: Risk classification (ResolveRisk), tool authorization (Authorizer.AuthorizeTool), and fail-closed policy compilation for unlinked/ambiguous attribution
  • Formal notation used: Z3-style guard conjunction / propositional logic

Formal Model

Predicates and invariants (illustrative notation)
;; P1 — RiskResolutionDeterminism
;; Source: "Risk classification" — ResolveRisk(intent) pseudocode
(assert (forall ((i IntentRecord))
  (= (ResolveRisk i) (ResolveRisk i))))  ; pure function, no hidden state

;; P2 — RiskExplicitOverride
;; Source: "if intent.Risk != "" { return intent.Risk }"
(assert (forall ((i IntentRecord))
  (=> (not (= (Risk i) ""))
      (= (ResolveRisk i) (Risk i)))))

;; P3 — RiskSecurityCriticalHigh
;; Source: "security + critical → high"
(assert (forall ((i IntentRecord))
  (=> (and (= (Risk i) "")
           (contains (Domains i) "security")
           (= (Priority i) "critical"))
      (= (ResolveRisk i) "high"))))

;; P4 — RiskProductionHigh
;; Source: "production → high"
(assert (forall ((i IntentRecord))
  (=> (and (= (Risk i) "") (contains (Domains i) "production"))
      (= (ResolveRisk i) "high"))))

;; P5 — RiskInfrastructureMedium
;; Source: "infrastructure → medium"
(assert (forall ((i IntentRecord))
  (=> (and (= (Risk i) "") (contains (Domains i) "infrastructure"))
      (= (ResolveRisk i) "medium"))))

;; P6 — RiskDocumentationLow
;; Source: "documentation → low"
(assert (forall ((i IntentRecord))
  (=> (and (= (Risk i) "") (contains (Domains i) "documentation"))
      (= (ResolveRisk i) "low"))))

;; P7 — RiskUnknownDefault
;; Source: "unknown → unknown" (fallthrough of ResolveRisk)
(assert (forall ((i IntentRecord))
  (=> (and (= (Risk i) "")
           (not (matches-any-rule i)))
      (= (ResolveRisk i) "unknown"))))

;; P8 — RiskPrecedenceOrder
;; Source: sequential if-chain in ResolveRisk pseudocode — first matching
;; guard wins; security+critical is evaluated before production,
;; infrastructure, and documentation.
(assert (forall ((i IntentRecord))
  (=> (and (contains (Domains i) "security") (= (Priority i) "critical")
           (contains (Domains i) "production")
           (contains (Domains i) "infrastructure")
           (contains (Domains i) "documentation"))
      (= (ResolveRisk i) "high"))))  ; via security+critical, not the other rules

;; P9 — AuthorizeToolDeniedWins
;; Source: "Enforcement" — AuthorizeTool: DeniedTools checked before AllowedTools
(assert (forall ((p ExecutionPolicy) (tool String))
  (=> (member tool (DeniedTools p))
      (= (AuthorizeTool p tool) ErrToolDenied))))

;; P10 — AuthorizeToolAllowlistGate
;; Source: "if !slices.Contains(policy.AllowedTools, tool) { return ErrToolNotAllowed }"
(assert (forall ((p ExecutionPolicy) (tool String))
  (=> (and (not (member tool (DeniedTools p)))
           (not (= (AllowedTools p) nil))
           (not (member tool (AllowedTools p))))
      (= (AuthorizeTool p tool) ErrToolNotAllowed))))

;; P11 — AuthorizeToolUnrestricted
;; Source: nil AllowedTools == unrestricted (pkg/intent/policy.go convention)
(assert (forall ((p ExecutionPolicy) (tool String))
  (=> (and (= (AllowedTools p) nil) (not (member tool (DeniedTools p))))
      (= (AuthorizeTool p tool) OK))))

;; P12 — AuthorizeToolEmptyDenyAll
;; Source: non-nil empty AllowedTools == deny-all (pkg/intent/policy.go convention)
(assert (forall ((p ExecutionPolicy) (tool String))
  (=> (= (AllowedTools p) (as-empty-non-nil-list))
      (= (AuthorizeTool p tool) ErrToolNotAllowed))))

;; P13 — SafestDefaultFailClosed
;; Source: "Unknown or ambiguous intent must not grant elevated authority."
;; Cross-checked against pkg/intent/policy.go PolicyCompiler.Compile
(assert (forall ((rec IntentRecord) (rules (List PolicyRule)))
  (=> (or (= (Status rec) Unlinked) (= (Status rec) Ambiguous))
      (= (Compile rec rules) SafestDefaultPolicy))))

Behavioral Coverage Map

Predicate / Invariant Test Function Description
P1/P2 RiskExplicitOverride TestResolveRisk_ExplicitOverride Explicit intent.Risk always wins over derived rules, even with conflicting domains/priority
P3 RiskSecurityCriticalHigh TestResolveRisk_SecurityCriticalIsHigh domains ∋ security ∧ priority = critical ⇒ high
P4 RiskProductionHigh TestResolveRisk_ProductionIsHigh domains ∋ production ⇒ high, independent of priority
P5 RiskInfrastructureMedium TestResolveRisk_InfrastructureIsMedium domains ∋ infrastructure ⇒ medium
P6 RiskDocumentationLow TestResolveRisk_DocumentationIsLow domains ∋ documentation ⇒ low
P7 RiskUnknownDefault TestResolveRisk_UnknownDefault No matching rule (empty, unrecognized domain, security w/o critical) ⇒ unknown
P8 RiskPrecedenceOrder TestResolveRisk_PrecedenceOrder Security+critical takes precedence when multiple domains overlap
P9 AuthorizeToolDeniedWins TestAuthorizeTool_DeniedWins Deny list wins even if tool also appears in allow list
P10 AuthorizeToolAllowlistGate TestAuthorizeTool_AllowlistGate Non-nil allow list rejects tools not listed
P11 AuthorizeToolUnrestricted TestAuthorizeTool_UnrestrictedWhenAllowedToolsNil nil AllowedTools ⇒ unrestricted (except explicit denies)
P12 AuthorizeToolEmptyDenyAll TestAuthorizeTool_EmptyAllowedToolsDeniesAll Non-nil empty AllowedTools ⇒ deny-all, distinct from nil
P13 SafestDefaultFailClosed TestSafestDefaultPolicy_FailClosedForIndeterminateStatus unlinked/ambiguous status forces safest policy regardless of configured rules
Edge: empty record TestEdgeCase_EmptyDomainsAndPriority Fully empty intent record resolves to unknown, not panic/empty string
Edge: nil tool lists TestEdgeCase_NilDeniedAndAllowedTools AuthorizeTool doesn't panic on zero-value policy
Edge: rule merge order TestEdgeCase_MultipleMatchingRulesPreserveStricterConstraint Stricter constraint from an earlier rule isn't overridden by a later lenient rule

Generated Test Suite

📄 pkg/intent/governance_formal_test.go
// Package intent_test provides a formal-methods-derived test suite for the
// Intent Attribution & Agent Governance Specification
// (specs/intent-attribution-agent-governance.md).
//
// This file encodes the following formal predicates as executable Go tests:
//
//	P1  RiskResolutionDeterminism   — ResolveRisk(intent) is a pure function of
//	                                  (Risk, Domains, Priority); no hidden state.
//	P2  RiskExplicitOverride        — if intent.Risk != "" then result == intent.Risk.
//	P3  RiskSecurityCriticalHigh    — domains ∋ security ∧ priority = critical ⇒ high.
//	P4  RiskProductionHigh          — domains ∋ production ⇒ high.
//	P5  RiskInfrastructureMedium    — domains ∋ infrastructure ⇒ medium.
//	P6  RiskDocumentationLow        — domains ∋ documentation ⇒ low.
//	P7  RiskUnknownDefault          — no matching domain/priority rule ⇒ unknown.
//	P8  RiskPrecedenceOrder         — security-critical takes precedence over
//	                                  production/infrastructure/documentation
//	                                  when multiple domains are present.
//	P9  AuthorizeToolDeniedWins     — tool ∈ DeniedTools ⇒ ErrToolDenied, even if
//	                                  also present in AllowedTools (deny-first).
//	P10 AuthorizeToolAllowlistGate  — tool ∉ AllowedTools (non-nil) ⇒ ErrToolNotAllowed.
//	P11 AuthorizeToolUnrestricted   — AllowedTools == nil ∧ tool ∉ DeniedTools ⇒ nil (ok).
//	P12 AuthorizeToolEmptyDenyAll   — AllowedTools == []string{} (non-nil empty) ⇒
//	                                  ErrToolNotAllowed for any tool (deny-all).
//	P13 SafestDefaultFailClosed     — safestDefaultPolicy() is at least as
//	                                  restrictive as any compiled policy for
//	                                  unlinked/ambiguous intents (cross-referenced
//	                                  against existing PolicyCompiler.Compile()).
package intent_test

import (
	"errors"
	"slices"
	"testing"

	"github.com/github/gh-aw/pkg/intent"
	"github.com/stretchr/testify/assert"
	"github.com/stretchr/testify/require"
)

// ---------------------------------------------------------------------------
// stub — replace with real implementation
//
// ResolveRisk and Authorizer.AuthorizeTool are specified in
// specs/intent-attribution-agent-governance.md ("Risk classification" and
// "Enforcement" sections) but are not yet implemented in pkg/intent. These
// stubs faithfully encode the pseudocode from the spec so the formal
// predicates below are testable today; delete the stubs once the real
// functions land in pkg/intent and re-point the tests at intent.ResolveRisk /
// intent.Authorizer.AuthorizeTool.
// ---------------------------------------------------------------------------

var (
	errToolDenied     = errors.New("tool denied")
	errToolNotAllowed = errors.New("tool not allowed")
)

type stubIntentRecord struct {
	Risk     string
	Domains  []string
	Priority string
}

func stubResolveRisk(rec stubIntentRecord) string {
	if rec.Risk != "" {
		return rec.Risk
	}
	if slices.Contains(rec.Domains, "security") && rec.Priority == "critical" {
		return "high"
	}
	if slices.Contains(rec.Domains, "production") {
		return "high"
	}
	if slices.Contains(rec.Domains, "infrastructure") {
		return "medium"
	}
	if slices.Contains(rec.Domains, "documentation") {
		return "low"
	}
	return "unknown"
}

func stubAuthorizeTool(policy intent.ExecutionPolicy, tool string) error {
	if slices.Contains(policy.DeniedTools, tool) {
		return errToolDenied
	}
	if policy.AllowedTools != nil && !slices.Contains(policy.AllowedTools, tool) {
		return errToolNotAllowed
	}
	return nil
}

// ---------------------------------------------------------------------------
// P1-P8: Risk classification (ResolveRisk)
// ---------------------------------------------------------------------------

// TestResolveRisk_ExplicitOverride encodes P1 and P2: ResolveRisk is a pure
// function of its input, and an explicit intent.Risk value always wins over
// any derived rule, regardless of Domains/Priority contents.
func TestResolveRisk_ExplicitOverride(t *testing.T) {
	tests := []struct {
		name string
		rec  stubIntentRecord
		want string
	}{
		{
			name: "explicit risk overrides security+critical derivation",
			rec:  stubIntentRecord{Risk: "low", Domains: []string{"security"}, Priority: "critical"},
			want: "low",
		},
		{
			name: "explicit risk overrides production derivation",
			rec:  stubIntentRecord{Risk: "medium", Domains: []string{"production"}},
			want: "medium",
		},
		{
			name: "explicit risk preserved even if unrecognized value",
			rec:  stubIntentRecord{Risk: "custom-tier"},
			want: "custom-tier",
		},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			got := stubResolveRisk(tt.rec)
			assert.Equal(t, tt.want, got, "explicit intent.Risk must take precedence over derived rules (P2)")
		})
	}
}

// TestResolveRisk_SecurityCriticalIsHigh encodes P3: domains containing
// "security" combined with priority "critical" must derive risk "high".
func TestResolveRisk_SecurityCriticalIsHigh(t *testing.T) {
	rec := stubIntentRecord{Domains: []string{"security"}, Priority: "critical"}
	got := stubResolveRisk(rec)
	require.Equal(t, "high", got, "security domain + critical priority must derive risk=high (P3)")
}

// TestResolveRisk_ProductionIsHigh encodes P4: production domain alone
// (independent of priority) must derive risk "high".
func TestResolveRisk_ProductionIsHigh(t *testing.T) {
	rec := stubIntentRecord{Domains: []string{"production"}, Priority: "low"}
	got := stubResolveRisk(rec)
	assert.Equal(t, "high", got, "production domain must derive risk=high regardless of priority (P4)")
}

// TestResolveRisk_InfrastructureIsMedium encodes P5.
func TestResolveRisk_InfrastructureIsMedium(t *testing.T) {
	rec := stubIntentRecord{Domains: []string{"infrastructure"}}
	got := stubResolveRisk(rec)
	assert.Equal(t, "medium", got, "infrastructure domain must derive risk=medium (P5)")
}

// TestResolveRisk_DocumentationIsLow encodes P6.
func TestResolveRisk_DocumentationIsLow(t *testing.T) {
	rec := stubIntentRecord{Domains: []string{"documentation"}}
	got := stubResolveRisk(rec)
	assert.Equal(t, "low", got, "documentation domain must derive risk=low (P6)")
}

// TestResolveRisk_UnknownDefault encodes P7: an intent with no explicit risk
// and no matching domain rule must default to "unknown" — never silently to
// an empty string or a permissive value.
func TestResolveRisk_UnknownDefault(t *testing.T) {
	tests := []struct {
		name string
		rec  stubIntentRecord
	}{
		{name: "no domains at all", rec: stubIntentRecord{}},
		{name: "unrecognized domain", rec: stubIntentRecord{Domains: []string{"marketing"}}},
		{name: "security domain without critical priority", rec: stubIntentRecord{Domains: []string{"security"}, Priority: "low"}},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			got := stubResolveRisk(tt.rec)
			assert.Equal(t, "unknown", got, "absence of explicit risk and matching rule must default to unknown, not empty or permissive (P7)")
		})
	}
}

// TestResolveRisk_PrecedenceOrder encodes P8: when multiple domains are
// present simultaneously, the security+critical rule takes precedence over
// production, infrastructure, and documentation rules (evaluated in the
// order given by the spec's Go pseudocode).
func TestResolveRisk_PrecedenceOrder(t *testing.T) {
	rec := stubIntentRecord{
		Domains:  []string{"documentation", "infrastructure", "production", "security"},
		Priority: "critical",
	}
	got := stubResolveRisk(rec)
	assert.Equal(t, "high", got, "security+critical must take precedence over production/infrastructure/documentation when domains overlap (P8)")
}

// ---------------------------------------------------------------------------
// P9-P12: Enforcement (AuthorizeTool)
// ---------------------------------------------------------------------------

// TestAuthorizeTool_DeniedWins encodes P9: a tool present in DeniedTools must
// be rejected with ErrToolDenied even if it is also present in AllowedTools
// (deny takes precedence over allow — fail closed).
func TestAuthorizeTool_DeniedWins(t *testing.T) {
	policy := intent.ExecutionPolicy{
		AllowedTools: []string{"read_file", "write_file"},
		DeniedTools:  []string{"write_file"},
	}
	err := stubAuthorizeTool(policy, "write_file")
	require.Error(t, err, "a tool present in both AllowedTools and DeniedTools must be denied (P9)")
	assert.ErrorIs(t, err, errToolDenied, "deny must take precedence over allow (P9)")
}

// TestAuthorizeTool_AllowlistGate encodes P10: when AllowedTools is a
// non-nil, non-empty list, any tool not present in it must be rejected with
// ErrToolNotAllowed.
func TestAuthorizeTool_AllowlistGate(t *testing.T) {
	policy := intent.ExecutionPolicy{
		AllowedTools: []string{"read_file"},
	}
	err := stubAuthorizeTool(policy, "exec_shell")
	require.Error(t, err, "a tool absent from a non-nil AllowedTools list must be rejected (P10)")
	assert.ErrorIs(t, err, errToolNotAllowed, "rejection reason must be ErrToolNotAllowed (P10)")
}

// TestAuthorizeTool_UnrestrictedWhenAllowedToolsNil encodes P11: a nil
// AllowedTools slice means "unrestricted" — any tool not explicitly denied
// must be authorized.
func TestAuthorizeTool_UnrestrictedWhenAllowedToolsNil(t *testing.T) {
	policy := intent.ExecutionPolicy{
		AllowedTools: nil,
		DeniedTools:  []string{"exec_shell"},
	}
	err := stubAuthorizeTool(policy, "read_file")
	assert.NoError(t, err, "nil AllowedTools must be treated as unrestricted for tools not explicitly denied (P11)")
}

// TestAuthorizeTool_EmptyAllowedToolsDeniesAll encodes P12: a non-nil, empty
// AllowedTools slice ([]string{}) must be treated as deny-all — distinct
// from a nil slice, which means unrestricted.
func TestAuthorizeTool_EmptyAllowedToolsDeniesAll(t *testing.T) {
	policy := intent.ExecutionPolicy{
		AllowedTools: []string{}, // non-nil empty: deny-all
	}
	err := stubAuthorizeTool(policy, "read_file")
	require.Error(t, err, "a non-nil empty AllowedTools slice must deny every tool (P12)")
	assert.ErrorIs(t, err, errToolNotAllowed, "empty (non-nil) AllowedTools must produce ErrToolNotAllowed (P12)")
}

// ---------------------------------------------------------------------------
// P13: Safe default is fail-closed for indeterminate attribution
// ---------------------------------------------------------------------------

// TestSafestDefaultPolicy_FailClosedForIndeterminateStatus encodes P13:
// PolicyCompiler.Compile must return the safest (most restrictive) policy
// whenever the resolved intent's attribution status is Unlinked or
// Ambiguous, regardless of any configured rules — unknown/ambiguous intent
// must never be granted elevated authority.
func TestSafestDefaultPolicy_FailClosedForIndeterminateStatus(t *testing.T) {
	// A permissive rule that would grant broad autonomy if it were allowed to match.
	permissiveRule := intent.PolicyRule{
		ID: "always-match",
		Set: intent.ExecutionPolicy{
			Autonomy:    "bounded",
			WriteScope:  "any_branch",
			MaxAttempts: 5,
		},
	}
	compiler := intent.PolicyCompiler{Rules: []intent.PolicyRule{permissiveRule}}

	tests := []struct {
		name   string
		status intent.AttributionStatus
	}{
		{name: "unlinked status forces safest default", status: intent.AttributionUnlinked},
		{name: "ambiguous status forces safest default", status: intent.AttributionAmbiguous},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			rec := intent.IntentRecord{Status: tt.status}
			got := compiler.Compile(rec, intent.RepositoryContext{})
			assert.Equal(t, "propose_only", got.Autonomy, "indeterminate attribution must fail closed to propose_only autonomy (P13)")
			assert.Equal(t, "none", got.WriteScope, "indeterminate attribution must fail closed to write_scope=none (P13)")
			assert.True(t, got.HumanApprovalRequired, "indeterminate attribution must require human approval (P13)")
			require.NotNil(t, got.AutoMergeAllowed, "AutoMergeAllowed must be explicitly set for the safe default (P13)")
			assert.False(t, *got.AutoMergeAllowed, "indeterminate attribution must deny auto-merge (P13)")
			assert.Equal(t, 1, got.MaxAttempts, "indeterminate attribution must cap max_attempts at 1 (P13)")
		})
	}
}

// ---------------------------------------------------------------------------
// Edge / error cases (Step 2 requirement: at least 3)
// ---------------------------------------------------------------------------

// TestEdgeCase_EmptyDomainsAndPriority verifies that ResolveRisk handles a
// completely empty record (no Risk, no Domains, no Priority) gracefully by
// returning "unknown" rather than panicking or returning an empty string.
func TestEdgeCase_EmptyDomainsAndPriority(t *testing.T) {
	rec := stubIntentRecord{}
	got := stubResolveRisk(rec)
	assert.Equal(t, "unknown", got, "an entirely empty intent record must resolve to unknown risk, not panic or empty string (edge case)")
}

// TestEdgeCase_NilDeniedAndAllowedTools verifies AuthorizeTool does not
// panic when both DeniedTools and AllowedTools are nil (fully unrestricted
// policy — e.g. a policy fragment that never set tool restrictions).
func TestEdgeCase_NilDeniedAndAllowedTools(t *testing.T) {
	policy := intent.ExecutionPolicy{}
	assert.NotPanics(t, func() {
		err := stubAuthorizeTool(policy, "any_tool")
		assert.NoError(t, err, "a policy with nil AllowedTools and nil DeniedTools must authorize any tool (edge case)")
	}, "AuthorizeTool must not panic on a zero-value ExecutionPolicy (edge case)")
}

// TestEdgeCase_MultipleMatchingRulesPreserveStricterConstraint verifies
// PolicyCompiler.Compile merges multiple matching rules using stricter-wins
// semantics rather than letting the last rule silently override a stricter
// earlier one (spec: "Policy merging must preserve stricter higher-precedence
// constraints").
func TestEdgeCase_MultipleMatchingRulesPreserveStricterConstraint(t *testing.T) {
	strict := intent.PolicyRule{
		ID:   "strict-rule",
		When: intent.PolicyCondition{Domain: "security"},
		Set: intent.ExecutionPolicy{
			Autonomy:    "propose_only",
			WriteScope:  "none",
			MaxAttempts: 1,
		},
	}
	lenient := intent.PolicyRule{
		ID:   "lenient-rule",
		When: intent.PolicyCondition{Priority: "critical"},
		Set: intent.ExecutionPolicy{
			Autonomy:    "bounded",
			WriteScope:  "any_branch",
			MaxAttempts: 10,
		},
	}
	compiler := intent.PolicyCompiler{Rules: []intent.PolicyRule{strict, lenient}}
	rec := intent.IntentRecord{
		Status: intent.AttributionMapped,
		Labels: []string{"security", "critical"},
	}
	got := compiler.Compile(rec, intent.RepositoryContext{})

	assert.Equal(t, "propose_only", got.Autonomy, "stricter propose_only autonomy from the security rule must not be overridden by the lenient rule's bounded autonomy (edge case)")
	assert.Equal(t, "none", got.WriteScope, "stricter write_scope=none must be preserved over the lenient rule's any_branch (edge case)")
	assert.Equal(t, 1, got.MaxAttempts, "the lower (stricter) max_attempts must win over the higher lenient value (edge case)")
	assert.ElementsMatch(t, []string{"strict-rule", "lenient-rule"}, got.RuleIDs, "both matching rule IDs must be recorded in provenance (edge case)")
}

Usage

  1. Copy the test file to pkg/intent/governance_formal_test.go.
  2. Replace the stub — marked stubResolveRisk and stubAuthorizeTool functions with real calls to intent.ResolveRisk(...) and intent.Authorizer{}.AuthorizeTool(...) once those are implemented (see the spec's "Authorizer.AuthorizeTool Implementation Audit" section for the required follow-up).
  3. Run: go test ./pkg/intent/... -run Formal

Context

Generated by 🔬 Daily Formal Spec Verifier · auto · 75.6 AIC · ⌖ 14.5 AIC · ⊞ 10.3K ·

  • expires on Aug 25, 2026, 7:47 AM UTC-08:00

Metadata

Metadata

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions