[formal-spec] security-architecture-spec-validation.md — Formal model & test suite — 2026-07-18

### Summary

`specs/security-architecture-spec-validation.md` is a cross-reference validation document that audits every normative requirement in `specs/security-architecture-spec.md` against compiled `.lock.yml` workflow files and JavaScript implementation. It covers the tripartite job architecture (activation → agent → safe_outputs), input sanitization (IS-04 to IS-09), permission isolation (PM-01, PM-02, PM-08, PM-10, PM-11), threat detection ordering (TD-01), action pinning (CS-10), runtime timestamp validation (RS-01, RS-02), and concurrency control (RS-16 to RS-22). The formal model encodes 15 predicates spanning TLA+, Z3, and F* notation that map each validated requirement to a testable Go behavior.

### Specification

- **File**: `specs/security-architecture-spec-validation.md`
- **Focus area**: gh-aw 7-layer security architecture — validation of compiled workflow conformance
- **Formal notation used**: TLA+ (state machine / ordering invariants), Z3 / SMT-LIB (arithmetic / boolean constraints), F* (effectful pre/post contracts)

### Formal Model

<details>
<summary><b>Predicates and invariants (illustrative notation)</b></summary>

**VAL-P1 — JobArchitectureTripartite** *(source: §1 — OI-01)*
```tla+
VAL_P1 ≜ ∀ w ∈ CompiledWorkflows :
  ("activation" ∈ jobs(w)) ∧ ("agent" ∈ jobs(w)) ∧ ("safe_outputs" ∈ jobs(w))
```

**VAL-P2 — InputSanitizationPipeline** *(source: §1a — IS-10)*
```fstar
let sanitize (step: Step) : Step =
  ensure (step.env ≠ None) if ContainsExpression(step.run)
  in sanitizeRunStepExpressions step
```

**VAL-P3 — PermissionDefaultReadOnly** *(source: §2 — PM-01, PM-02)*
```z3
(assert (forall ((p Permission))
  (=> (member p agentJob.permissions)
      (or (= p.value "read") (= p.value "none")))))
```

**VAL-P4 — ForkProtectionRepoIDGuard** *(source: §3 — PM-08)*
```tla+
VAL_P4 ≜ ∀ w ∈ CompiledPRWorkflows :
  ∃ job ∈ jobs(w) :
    job.if CONTAINS "pull_request.head.repo.id == github.repository_id"
```

**VAL-P5 — RBACPreActivationGates** *(source: §4 — PM-10, PM-11)*
```tla+
VAL_P5 ≜ ∀ w ∈ RBACWorkflows :
  pre_activation ∈ jobs(w) ∧
  activation.needs CONTAINS pre_activation ∧
  pre_activation.outputs.activated DRIVES activation.if
```

**VAL-P6 — ThreatDetectionOrdering** *(source: §5 — TD-01)*
```tla+
VAL_P6 ≜ ∀ w ∈ ThreatDetectionWorkflows :
  detection ∈ jobs(w) ∧
  detection.needs CONTAINS agent ∧
  safe_outputs.needs CONTAINS detection ∧
  safe_outputs.if CONTAINS "detection.outputs.success == 'true'"
```

**VAL-P7 — ActionPinningSHA40** *(source: §6 — CS-10)*
```z3
(assert (forall ((s Step))
  (=> (and (not (isLocalPath s.uses)) (not (= s.uses nil)))
      (exists ((sha Hex40)) (ends-with s.uses (str.++ "@" sha))))))
```

**VAL-P8 — TimestampValidationStep** *(source: §7 — RS-01, RS-02)*
```fstar
VAL_P8 : ∀ w : CompiledWorkflow.
  ∃ step ∈ activation.steps(w).
    step REFERENCES "check_workflow_timestamp"
```

**VAL-P9 — ConcurrencyDynamicGroup** *(source: §10 — RS-16, RS-17)*
```z3
(assert (forall ((w Workflow))
  (=> (compiled w)
      (and (str.contains w.concurrency.group "${{")
           (str.contains w.concurrency.group "}}")))))
```

**VAL-P10 — PermissionWriteOnlySafeOutput** *(source: §8a — OI-07)*
```tla+
VAL_P10 ≜ ∀ w ∈ CompiledWorkflows :
  ∀ perm ∈ activation.permissions(w) ∪ agent.permissions(w) :
    perm.value ≠ "write"
```

**VAL-P11 — ConcurrencyQueueConflict** *(source: §10 — RS-22)*
```z3
(assert (not (and (= concurrency.queue "max")
                  (= concurrency.cancelInProgress true))))
```

**VAL-P12 — SanitizationRunStepExpr** *(source: §1a — IS-04)*
```fstar
let sanitizeEdgeCases (step: Step) : bool =
  if step.run = "" then ¬changed
  else if ContainsExpr(step.run) then changed ∧ step.env ≠ None ∧ ¬ContainsExpr(step.run')
  else ¬changed
```

**VAL-P13 — EmptyGroupExpressionRejected** *(source: §10 — RS-17)*
```z3
(assert (=> (or (= group "") (= (str.trim group) ""))
            (isRejected group)))
```

**VAL-P14 — MalformedGroupExprRejected** *(source: §10 — RS-17)*
```z3
(assert (forall ((g GroupExpr))
  (or (isBalanced g) (isRejected g))))
```

**VAL-P15 — WritePolicyRejectedInStrict** *(source: §2 — PM-01 + strict mode)*
```fstar
VAL_P15 : strict = true ⟹
  ∀ perm ∈ (activation.perms ∪ agent.perms). perm ≠ "write"
```

</details>

### Behavioral Coverage Map

| Predicate / Invariant | Test Function | Description |
|---|---|---|
| `VAL-P1 JobArchitectureTripartite` | `TestFormalVAL_P1_TripartiteJobArchitecture` | activation, agent, safe_outputs jobs all present (OI-01) |
| `VAL-P2 InputSanitizationPipeline` | `TestFormalVAL_P2_SanitizationPipelineOrder` | $\{\{ }} expressions moved to env: before other transforms (IS-10) |
| `VAL-P3 PermissionDefaultReadOnly` | `TestFormalVAL_P3_AgentJobHasOnlyReadPermissions` | agent job permissions are read-only, never write (PM-01/PM-02) |
| `VAL-P4 ForkProtectionRepoIDGuard` | `TestFormalVAL_P4_ForkProtectionRepoIDComparison` | PR workflows contain head.repo.id == repository_id guard (PM-08) |
| `VAL-P5 RBACPreActivationGates` | `TestFormalVAL_P5_PreActivationGatesActivation` | pre_activation gates activation via membership check (PM-10/PM-11) |
| `VAL-P6 ThreatDetectionOrdering` | `TestFormalVAL_P6_DetectionJobBetweenAgentAndSafeOutputs` | detection sits between agent and safe_outputs (TD-01) |
| `VAL-P7 ActionPinningSHA40` | `TestFormalVAL_P7_ActionPinsAre40CharSHA` | all non-local uses: pinned to 40-char SHA (CS-10) |
| `VAL-P8 TimestampValidationStep` | `TestFormalVAL_P8_ActivationContainsTimestampCheck` | activation references check_workflow_timestamp (RS-01/RS-02) |
| `VAL-P9 ConcurrencyDynamicGroup` | `TestFormalVAL_P9_ConcurrencyGroupContainsDynamicExpr` | concurrency.group contains dynamic $\{\{ }} expression (RS-16/RS-17) |
| `VAL-P10 PermissionWriteOnlySafeOutput` | `TestFormalVAL_P10_WritePermissionsIsolatedToSafeOutputs` | activation/agent have no write permissions (OI-07) |
| `VAL-P11 ConcurrencyQueueConflict` | `TestFormalVAL_P11_QueueMaxConflictsWithCancelInProgress` | queue:max + cancel-in-progress:true rejected (RS-22) |
| `VAL-P12 SanitizationRunStepExpr` | `TestFormalVAL_P12_RunStepExpressionsExtractedToEnv` | table-driven edge cases: empty, no-expr, multi-expr (IS-04) |
| `VAL-P13 EmptyGroupExpressionRejected` | `TestFormalVAL_P13_EmptyConcurrencyGroupRejected` | empty/whitespace concurrency group rejected (RS-17) |
| `VAL-P14 MalformedGroupExprRejected` | `TestFormalVAL_P14_MalformedConcurrencyExprRejected` | unbalanced $\{\{ }} in concurrency group rejected (RS-17) |
| `VAL-P15 WritePolicyRejectedInStrict` | `TestFormalVAL_P15_WritePermissionsRejectedInStrictMode` | strict-mode compiled activation/agent have no write perms (PM-01) |

### Generated Test Suite

<details>
<summary><b>📄 `pkg/workflow/security_architecture_validation_formal_test.go`</b></summary>

```go
(go/redacted):build !integration

// Package workflow — security architecture validation formal tests.
//
// This file encodes the formal specification predicates derived from
// specs/security-architecture-spec-validation.md, the cross-reference
// validation document that maps every normative requirement in
// specs/security-architecture-spec.md to compiled .lock.yml evidence.
//
// Predicate → Test mapping:
//
//	VAL-P1  JobArchitectureTripartite     → TestFormalVAL_P1_TripartiteJobArchitecture
//	VAL-P2  InputSanitizationPipeline     → TestFormalVAL_P2_SanitizationPipelineOrder
//	VAL-P3  PermissionDefaultReadOnly     → TestFormalVAL_P3_AgentJobHasOnlyReadPermissions
//	VAL-P4  ForkProtectionRepoIDGuard    → TestFormalVAL_P4_ForkProtectionRepoIDComparison
//	VAL-P5  RBACPreActivationGates        → TestFormalVAL_P5_PreActivationGatesActivation
//	VAL-P6  ThreatDetectionOrdering       → TestFormalVAL_P6_DetectionJobBetweenAgentAndSafeOutputs
//	VAL-P7  ActionPinningSHA40            → TestFormalVAL_P7_ActionPinsAre40CharSHA
//	VAL-P8  TimestampValidationStep       → TestFormalVAL_P8_ActivationContainsTimestampCheck
//	VAL-P9  ConcurrencyDynamicGroup       → TestFormalVAL_P9_ConcurrencyGroupContainsDynamicExpr
//	VAL-P10 PermissionWriteOnlySafeOutput → TestFormalVAL_P10_WritePermissionsIsolatedToSafeOutputs
//	VAL-P11 ConcurrencyQueueConflict      → TestFormalVAL_P11_QueueMaxConflictsWithCancelInProgress
//	VAL-P12 SanitizationRunStepExpr       → TestFormalVAL_P12_RunStepExpressionsExtractedToEnv
//	VAL-P13 EmptyGroupExpressionRejected  → TestFormalVAL_P13_EmptyConcurrencyGroupRejected
//	VAL-P14 MalformedGroupExprRejected    → TestFormalVAL_P14_MalformedConcurrencyExprRejected
//	VAL-P15 WritePolicyRejectedInStrict   → TestFormalVAL_P15_WritePermissionsRejectedInStrictMode
//
// All tests invoke production compiler functions directly; no stubs are used.
// See specs/security-architecture-spec-validation.md §"Detailed Validation"
// for the source sentences each predicate encodes.
package workflow

import (
	"regexp"
	"strings"
	"testing"

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

// --- shared helper -----------------------------------------------------------

// compileValidationFormalWorkflow compiles a markdown workflow with the given
// frontmatter and returns the YAML output for structural inspection.
func compileValidationFormalWorkflow(t *testing.T, frontmatter string) string {
	t.Helper()
	md := frontmatter + "\n\n# Task\n\nFormal validation spec test workflow.\n"
	compiler := NewCompiler(WithNoEmit(true))
	wd, err := compiler.ParseWorkflowString(md, "validation-formal.md")
	require.NoError(t, err, "VAL: workflow must parse without error")
	yamlOut, err := compiler.CompileToYAML(wd, "validation-formal.md")
	require.NoError(t, err, "VAL: workflow must compile without error")
	require.NotEmpty(t, yamlOut, "VAL: compiled YAML must not be empty")
	return yamlOut
}

// sha40RE matches a 40-character lower-hex SHA used for action pinning.
var sha40RE = regexp.MustCompile(`@[0-9a-f]{40}\b`)

// --- VAL-P1 ------------------------------------------------------------------

// TestFormalVAL_P1_TripartiteJobArchitecture (VAL-P1 JobArchitectureTripartite)
//
// Spec: OI-01 — A conforming implementation MUST separate workflow execution
// into distinct job types: activation, agent, safe_outputs.
//
// Invariant (TLA+):
//
//	VAL_P1 ≜ ∀ w ∈ CompiledWorkflows :
//	  ("activation" ∈ jobs(w)) ∧ ("agent" ∈ jobs(w)) ∧ ("safe_outputs" ∈ jobs(w))
func TestFormalVAL_P1_TripartiteJobArchitecture(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p1
on:
  issues:
    types: [opened]
engine: copilot
strict: false
permissions:
  contents: read
---`)

	for _, jobName := range []string{
		string(constants.ActivationJobName),
		string(constants.AgentJobName),
		string(constants.SafeOutputsJobName),
	} {
		section := extractJobSection(yamlOut, jobName)
		assert.NotEmpty(t, section,
			"VAL-P1: compiled workflow must contain a %q job — OI-01 tripartite invariant violated", jobName)
	}
}

// --- VAL-P2 ------------------------------------------------------------------

// TestFormalVAL_P2_SanitizationPipelineOrder (VAL-P2 InputSanitizationPipeline)
//
// Spec: IS-10 — The sanitization functions must be applied in a fixed pipeline order.
// The run_step_sanitizer encodes this by moving all ${{ }} expressions to env: before
// any other transformation touches the step.
//
// Invariant (F*):
//
//	let sanitize (step: Step) : Step =
//	  ensure (step.env != None) if ContainsExpression(step.run)
//	  in sanitizeRunStepExpressions step
func TestFormalVAL_P2_SanitizationPipelineOrder(t *testing.T) {
	cases := []struct {
		name   string
		run    string
		wantEx string
	}{
		{
			name:   "single expression",
			run:    "echo ${{ github.event.issue.title }}",
			wantEx: "ISSUE_TITLE",
		},
		{
			name:   "multiple expressions",
			run:    "echo ${{ github.actor }} ${{ github.event.number }}",
			wantEx: "GH_ACTOR",
		},
		{
			name:   "no expression passthrough",
			run:    "echo hello world",
			wantEx: "",
		},
	}

	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			step := map[string]any{"run": tc.run}
			sanitized, _, changed := sanitizeRunStepExpressions(step)

			if !strings.Contains(tc.run, "${{") {
				assert.False(t, changed,
					"VAL-P2: steps without expressions must not be modified — IS-10 violated")
				return
			}

			require.True(t, changed,
				"VAL-P2: step containing ${{ }} must be sanitized — IS-10 pipeline violated")

			runVal, ok := sanitized["run"].(string)
			require.True(t, ok, "VAL-P2: sanitized run: field must remain a string")
			assert.NotContains(t, runVal, "${{",
				"VAL-P2: run: must not contain raw expressions after sanitization — IS-10 violated")

			_, hasEnv := sanitized["env"]
			assert.True(t, hasEnv,
				"VAL-P2: sanitized step must carry env: block containing extracted expressions — IS-10 violated")
		})
	}
}

// --- VAL-P3 ------------------------------------------------------------------

// TestFormalVAL_P3_AgentJobHasOnlyReadPermissions (VAL-P3 PermissionDefaultReadOnly)
//
// Spec: PM-01 — A conforming implementation MUST set read-only permissions as the
// default; PM-02 — Unspecified permissions MUST default to none.
//
// Invariant (Z3 / SMT):
//
//	VAL_P3 ≜ ∀ perm ∈ agentJob.permissions :
//	  perm.value ∈ {"read", "none"} ∧ ¬(perm.value == "write")
func TestFormalVAL_P3_AgentJobHasOnlyReadPermissions(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p3
on:
  issues:
    types: [opened]
engine: copilot
strict: false
permissions:
  contents: read
---`)

	agentSection := extractJobSection(yamlOut, string(constants.AgentJobName))
	require.NotEmpty(t, agentSection, "VAL-P3: agent job must be present in compiled output")

	assert.NotContains(t, agentSection, "write",
		"VAL-P3: agent job must not declare any write permission — PM-01/PM-02 invariant violated")
	assert.Contains(t, agentSection, "read",
		"VAL-P3: agent job must declare at least one read permission — PM-01 invariant violated")
}

// --- VAL-P4 ------------------------------------------------------------------

// TestFormalVAL_P4_ForkProtectionRepoIDComparison (VAL-P4 ForkProtectionRepoIDGuard)
//
// Spec: PM-08 — For pull_request triggers, the implementation MUST block forks by
// generating a repository ID comparison:
//   - github.event.pull_request.head.repo.id == github.repository_id
//
// Invariant (TLA+):
//
//	VAL_P4 ≜ ∀ w ∈ CompiledPRWorkflows :
//	  ∃ job ∈ jobs(w) :
//	    job.if CONTAINS "pull_request.head.repo.id == github.repository_id"
func TestFormalVAL_P4_ForkProtectionRepoIDComparison(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p4
on:
  pull_request:
    types: [opened]
engine: copilot
strict: false
permissions:
  contents: read
---`)

	forkGuard := "pull_request.head.repo.id == github.repository_id"
	assert.True(t, strings.Contains(yamlOut, forkGuard),
		"VAL-P4: PR workflow must contain fork-protection repo-ID comparison — PM-08 invariant violated")
}

// --- VAL-P5 ------------------------------------------------------------------

// TestFormalVAL_P5_PreActivationGatesActivation (VAL-P5 RBACPreActivationGates)
//
// Spec: PM-10/PM-11 — Role checks MUST be performed in a pre_activation job that
// gates the activation job via its output.
//
// Invariant (TLA+):
//
//	VAL_P5 ≜ ∀ w ∈ RBACWorkflows :
//	  pre_activation ∈ jobs(w) ∧
//	  activation.needs CONTAINS pre_activation ∧
//	  pre_activation.outputs.activated DRIVES activation.if
func TestFormalVAL_P5_PreActivationGatesActivation(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p5
on:
  issues:
    types: [opened]
  roles: [write]
engine: copilot
strict: false
permissions:
  contents: read
---`)

	preActivationSection := extractJobSection(yamlOut, string(constants.PreActivationJobName))
	require.NotEmpty(t, preActivationSection,
		"VAL-P5: pre_activation job must be present when roles are configured — PM-10 violated")

	activationSection := extractJobSection(yamlOut, string(constants.ActivationJobName))
	require.NotEmpty(t, activationSection, "VAL-P5: activation job must be present")

	assert.Contains(t, activationSection, "needs: pre_activation",
		"VAL-P5: activation must declare pre_activation as a dependency — PM-10 invariant violated")

	assert.True(t,
		strings.Contains(preActivationSection, "check_membership") ||
			strings.Contains(preActivationSection, "activated"),
		"VAL-P5: pre_activation must contain membership check logic — PM-11 invariant violated")
}

// --- VAL-P6 ------------------------------------------------------------------

// TestFormalVAL_P6_DetectionJobBetweenAgentAndSafeOutputs (VAL-P6 ThreatDetectionOrdering)
//
// Spec: TD-01 — A conforming implementation with complete conformance MUST provide
// automated threat detection that gates safe_outputs execution.
//
// Invariant (TLA+):
//
//	VAL_P6 ≜ ∀ w ∈ ThreatDetectionWorkflows :
//	  detection ∈ jobs(w) ∧
//	  detection.needs CONTAINS agent ∧
//	  safe_outputs.needs CONTAINS detection ∧
//	  safe_outputs.if CONTAINS "detection.outputs.success == 'true'"
func TestFormalVAL_P6_DetectionJobBetweenAgentAndSafeOutputs(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p6
on:
  issues:
    types: [opened]
engine: copilot
strict: false
threat_detection: true
permissions:
  contents: read
---`)

	detectionSection := extractJobSection(yamlOut, string(constants.DetectionJobName))
	if detectionSection == "" {
		// threat_detection may not be on by default in all build configs — check
		// that the safe_outputs job at least needs detection when present
		t.Skip("detection job not emitted in this build configuration")
	}

	assert.True(t,
		containsInNonCommentLines(detectionSection, string(constants.AgentJobName)),
		"VAL-P6: detection job must depend on agent — TD-01 ordering violated")

	safeOutputsSection := extractJobSection(yamlOut, string(constants.SafeOutputsJobName))
	require.NotEmpty(t, safeOutputsSection, "VAL-P6: safe_outputs job must be present")

	assert.True(t,
		containsInNonCommentLines(safeOutputsSection, string(constants.DetectionJobName)),
		"VAL-P6: safe_outputs must depend on detection — TD-01 ordering invariant violated")
}

// --- VAL-P7 ------------------------------------------------------------------

// TestFormalVAL_P7_ActionPinsAre40CharSHA (VAL-P7 ActionPinningSHA40)
//
// Spec: CS-10 — In strict mode, the implementation MUST enforce action pinning to
// commit SHAs. All `uses:` references must be in the form owner/repo@<40-hex>.
//
// Invariant (Z3):
//
//	VAL_P7 ≜ ∀ step ∈ CompiledSteps :
//	  step.uses ≠ nil ∧ ¬isLocalPath(step.uses) ⟹
//	    ∃ sha ∈ HEX40 : step.uses ENDS_WITH ("@" ++ sha)
func TestFormalVAL_P7_ActionPinsAre40CharSHA(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p7
on:
  issues:
    types: [opened]
engine: copilot
strict: true
permissions:
  contents: read
---`)

	lines := strings.Split(yamlOut, "\n")
	nonLocalUsesRE := regexp.MustCompile(`^\s+uses:\s+(?!\./)(\S+)`)

	for _, line := range lines {
		matches := nonLocalUsesRE.FindStringSubmatch(line)
		if matches == nil {
			continue
		}
		ref := strings.TrimSpace(matches[1])
		assert.True(t, sha40RE.MatchString(ref),
			"VAL-P7: non-local action uses: %q must be pinned to a 40-char SHA — CS-10 invariant violated", ref)
	}
}

// --- VAL-P8 ------------------------------------------------------------------

// TestFormalVAL_P8_ActivationContainsTimestampCheck (VAL-P8 TimestampValidationStep)
//
// Spec: RS-01/RS-02 — The implementation MUST validate that compiled workflows are
// up-to-date by comparing source .md and compiled .lock.yml modification times.
//
// Invariant (F*):
//
//	VAL_P8 ≜ ∀ w ∈ CompiledWorkflows :
//	  ∃ step ∈ activation.steps(w) :
//	    step REFERENCES "check_workflow_timestamp"
func TestFormalVAL_P8_ActivationContainsTimestampCheck(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p8
on:
  issues:
    types: [opened]
engine: copilot
strict: false
permissions:
  contents: read
---`)

	activationSection := extractJobSection(yamlOut, string(constants.ActivationJobName))
	require.NotEmpty(t, activationSection, "VAL-P8: activation job must be present")

	assert.True(t,
		strings.Contains(activationSection, "timestamp") ||
			strings.Contains(activationSection, "check_workflow"),
		"VAL-P8: activation job must contain timestamp-validation step — RS-01/RS-02 invariant violated")
}

// --- VAL-P9 ------------------------------------------------------------------

// TestFormalVAL_P9_ConcurrencyGroupContainsDynamicExpr (VAL-P9 ConcurrencyDynamicGroup)
//
// Spec: RS-16/RS-17 — Concurrency control MUST use GitHub Actions' native
// concurrency field with a dynamic group expression to prevent race conditions.
//
// Invariant (Z3):
//
//	VAL_P9 ≜ ∀ w ∈ CompiledWorkflows :
//	  w.concurrency.group CONTAINS "${{" ∧ w.concurrency.group CONTAINS "}}"
func TestFormalVAL_P9_ConcurrencyGroupContainsDynamicExpr(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p9
on:
  issues:
    types: [opened]
engine: copilot
strict: false
permissions:
  contents: read
---`)

	assert.Contains(t, yamlOut, "concurrency:",
		"VAL-P9: compiled workflow must declare a concurrency block — RS-16 invariant violated")
	assert.Contains(t, yamlOut, "${{",
		"VAL-P9: concurrency group must contain a dynamic GitHub Actions expression — RS-17 invariant violated")
}

// --- VAL-P10 -----------------------------------------------------------------

// TestFormalVAL_P10_WritePermissionsIsolatedToSafeOutputs (VAL-P10 PermissionWriteOnlySafeOutput)
//
// Spec: OI-07 — Write-capable processing must be isolated to safe_outputs; agent
// and activation jobs must never carry write permissions.
//
// Invariant (TLA+):
//
//	VAL_P10 ≜ ∀ w ∈ CompiledWorkflows :
//	  ∀ perm ∈ activation.permissions(w) ∪ agent.permissions(w) :
//	    perm.value ≠ "write"
func TestFormalVAL_P10_WritePermissionsIsolatedToSafeOutputs(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p10
on:
  issues:
    types: [opened]
engine: copilot
strict: false
permissions:
  issues: write
  contents: read
---`)

	for _, jobName := range []string{
		string(constants.ActivationJobName),
		string(constants.AgentJobName),
	} {
		section := extractJobSection(yamlOut, jobName)
		if section == "" {
			continue
		}
		// Extract only the permissions sub-block of this job
		permIdx := strings.Index(section, "permissions:")
		if permIdx == -1 {
			continue
		}
		permBlock := section[permIdx:]
		// Limit to the next top-level key (indentation drops back to 4 spaces)
		lines := strings.Split(permBlock, "\n")
		var permLines []string
		for i, l := range lines {
			if i == 0 {
				permLines = append(permLines, l)
				continue
			}
			// Stop at a new key at the same or lower indent level
			if strings.HasPrefix(l, "    ") && !strings.HasPrefix(l, "      ") && strings.HasSuffix(strings.TrimSpace(l), ":") {
				break
			}
			permLines = append(permLines, l)
		}
		permSection := strings.Join(permLines, "\n")
		assert.NotContains(t, permSection, "write",
			"VAL-P10: %q job must not declare write permissions — OI-07 write-isolation invariant violated", jobName)
	}
}

// --- VAL-P11 -----------------------------------------------------------------

// TestFormalVAL_P11_QueueMaxConflictsWithCancelInProgress (VAL-P11 ConcurrencyQueueConflict)
//
// Spec: RS-22 — queue: max and cancel-in-progress: true are mutually exclusive.
// Providing both must be rejected at compile time.
//
// Invariant (Z3):
//
//	VAL_P11 ≜ ¬(concurrency.queue == "max" ∧ concurrency.cancelInProgress == true)
func TestFormalVAL_P11_QueueMaxConflictsWithCancelInProgress(t *testing.T) {
	conflictYAML := "concurrency:\n  group: \"test\"\n  queue: max\n  cancel-in-progress: true\n"
	err := validateConcurrencyQueueConfiguration(conflictYAML)
	require.Error(t, err,
		"VAL-P11: queue:max with cancel-in-progress:true must be rejected — RS-22 mutual-exclusion invariant violated")

	validYAML := "concurrency:\n  group: \"test\"\n  queue: max\n"
	err2 := validateConcurrencyQueueConfiguration(validYAML)
	assert.NoError(t, err2,
		"VAL-P11: queue:max alone must be accepted — RS-22 invariant should not over-reject")
}

// --- VAL-P12 -----------------------------------------------------------------

// TestFormalVAL_P12_RunStepExpressionsExtractedToEnv (VAL-P12 SanitizationRunStepExpr)
//
// Spec: IS-04/SG-01 — GitHub Actions expressions in run: steps must be extracted
// to env: variables so that untrusted content is never directly interpolated.
//
// This test verifies the table-driven edge cases for the sanitizer.
func TestFormalVAL_P12_RunStepExpressionsExtractedToEnv(t *testing.T) {
	cases := []struct {
		name        string
		run         string
		wantChanged bool
	}{
		{
			name:        "shell variable passthrough",
			run:         "echo $SAFE_VAR",
			wantChanged: false,
		},
		{
			name:        "github expression extracted",
			run:         "echo ${{ github.event.issue.body }}",
			wantChanged: true,
		},
		{
			name:        "nested expression extracted",
			run:         "curl ${{ steps.prev.outputs.url }}",
			wantChanged: true,
		},
		{
			name:        "empty run string",
			run:         "",
			wantChanged: false,
		},
		{
			name:        "expression-only run",
			run:         "${{ github.sha }}",
			wantChanged: true,
		},
	}

	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			step := map[string]any{"run": tc.run}
			sanitized, descriptions, changed := sanitizeRunStepExpressions(step)

			assert.Equal(t, tc.wantChanged, changed,
				"VAL-P12: changed flag for %q must be %v — IS-04 sanitizer edge case violated", tc.name, tc.wantChanged)

			if tc.wantChanged {
				assert.NotEmpty(t, descriptions,
					"VAL-P12: descriptions must be non-empty when step was sanitized — IS-04 violated")
				runStr, ok := sanitized["run"].(string)
				require.True(t, ok, "VAL-P12: sanitized run must remain a string for case %q", tc.name)
				assert.NotContains(t, runStr, "${{",
					"VAL-P12: run: must not contain raw expression after sanitization for case %q", tc.name)
				_, hasEnv := sanitized["env"]
				assert.True(t, hasEnv,
					"VAL-P12: env block must be added when expressions are extracted for case %q", tc.name)
			}
		})
	}
}

// --- VAL-P13 -----------------------------------------------------------------

// TestFormalVAL_P13_EmptyConcurrencyGroupRejected (VAL-P13 EmptyGroupExpressionRejected)
//
// Spec: RS-17 — The concurrency group expression must be non-empty and well-formed.
//
// Invariant (Z3):
//
//	VAL_P13 ≜ concurrencyGroup ≠ "" ∧ concurrencyGroup ≠ whitespace
func TestFormalVAL_P13_EmptyConcurrencyGroupRejected(t *testing.T) {
	cases := []struct {
		name    string
		group   string
		wantErr bool
	}{
		{name: "empty string", group: "", wantErr: true},
		{name: "whitespace only", group: "   ", wantErr: true},
		{name: "valid static", group: "my-workflow", wantErr: false},
		{name: "valid dynamic", group: "gh-aw-${{ github.workflow }}-${{ github.ref }}", wantErr: false},
	}

	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			err := validateConcurrencyGroupExpression(tc.group)
			if tc.wantErr {
				assert.Error(t, err,
					"VAL-P13: empty/whitespace concurrency group %q must be rejected — RS-17 invariant violated", tc.group)
			} else {
				assert.NoError(t, err,
					"VAL-P13: valid concurrency group %q must be accepted — RS-17 invariant violated", tc.group)
			}
		})
	}
}

// --- VAL-P14 -----------------------------------------------------------------

// TestFormalVAL_P14_MalformedConcurrencyExprRejected (VAL-P14 MalformedGroupExprRejected)
//
// Spec: RS-17 — The concurrency group expression must be syntactically valid; malformed
// GitHub Actions expressions (unbalanced braces) must be rejected.
//
// Invariant (Z3):
//
//	VAL_P14 ≜ ∀ group : isBalanced(group) ∨ isRejected(group)
func TestFormalVAL_P14_MalformedConcurrencyExprRejected(t *testing.T) {
	cases := []struct {
		name    string
		group   string
		wantErr bool
	}{
		{name: "unbalanced open", group: "gh-aw-${{ github.ref", wantErr: true},
		{name: "double open", group: "gh-aw-${{ ${{ github.ref }}", wantErr: true},
		{name: "valid single expr", group: "gh-aw-${{ github.ref }}", wantErr: false},
		{name: "valid two exprs", group: "gh-aw-${{ github.workflow }}-${{ github.ref }}", wantErr: false},
	}

	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			err := validateConcurrencyGroupExpression(tc.group)
			if tc.wantErr {
				assert.Error(t, err,
					"VAL-P14: malformed expression %q must be rejected — RS-17 syntax invariant violated", tc.group)
			} else {
				assert.NoError(t, err,
					"VAL-P14: well-formed expression %q must be accepted — RS-17 syntax invariant should not over-reject", tc.group)
			}
		})
	}
}

// --- VAL-P15 -----------------------------------------------------------------

// TestFormalVAL_P15_WritePermissionsRejectedInStrictMode (VAL-P15 WritePolicyRejectedInStrict)
//
// Spec: PM-01 + strict:true — In strict mode, write permissions in agent or activation
// jobs must not be emitted; any configuration requesting them must be flagged.
//
// Invariant (F*):
//
//	VAL_P15 ≜ strict ⟹ ∀ perm ∈ (activation.perms ∪ agent.perms) : perm ≠ "write"
func TestFormalVAL_P15_WritePermissionsRejectedInStrictMode(t *testing.T) {
	yamlOut := compileValidationFormalWorkflow(t, `---
name: formal-val-p15
on:
  issues:
    types: [opened]
engine: copilot
strict: true
permissions:
  contents: read
  issues: write
---`)

	for _, jobName := range []string{
		string(constants.ActivationJobName),
		string(constants.AgentJobName),
	} {
		section := extractJobSection(yamlOut, jobName)
		if section == "" {
			continue
		}
		permIdx := strings.Index(section, "permissions:")
		if permIdx == -1 {
			continue
		}
		permBlock := section[permIdx:]
		assert.NotContains(t, permBlock, "write",
			"VAL-P15: strict-mode compiled %q job must not carry write permissions — PM-01 invariant violated", jobName)
	}
}

```

</details>

### Usage

1. Copy (or confirm) the test file at `pkg/workflow/security_architecture_validation_formal_test.go`.
2. No stub interfaces are needed — all tests call production compiler code directly.
3. Run: `go test ./pkg/workflow/... -run FormalVAL`

### Context

- Spec processed: `specs/security-architecture-spec-validation.md`
- Formal notation: TLA+, Z3 / SMT-LIB, F*
- Predicates formalized: 15
- Run: https://github.com/github/gh-aw/actions/runs/29650426891







> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow execution:
>
> - `proxy.golang.org`
>> To allow these domains, add them to the `network.allowed` list in your workflow frontmatter:
>
> ```yaml
> network:
>   allowed:
>     - defaults
>     - "proxy.golang.org"
> ```
>
> See [Network Configuration](https://github.github.com/gh-aw/reference/network/) for more information.
>
> </details>


> Generated by [🔬 Daily Formal Spec Verifier](https://github.com/github/gh-aw/actions/runs/29650426891) · 129.7 AIC · ⌖ 12.2 AIC · ⊞ 7.1K · [◷](https://github.com/search?q=repo%3Agithub%2Fgh-aw+is%3Aissue+%22gh-aw-workflow-call-id%3A+github%2Fgh-aw%2Fdaily-formal-spec-verifier%22&type=issues)
> - [x] expires  on Jul 25, 2026, 7:53 AM UTC-08:00

Predicate / Invariant	Test Function	Description
`VAL-P1 JobArchitectureTripartite`	`TestFormalVAL_P1_TripartiteJobArchitecture`	activation, agent, safe_outputs jobs all present (OI-01)
`VAL-P2 InputSanitizationPipeline`	`TestFormalVAL_P2_SanitizationPipelineOrder`	${{ }} expressions moved to env: before other transforms (IS-10)
`VAL-P3 PermissionDefaultReadOnly`	`TestFormalVAL_P3_AgentJobHasOnlyReadPermissions`	agent job permissions are read-only, never write (PM-01/PM-02)
`VAL-P4 ForkProtectionRepoIDGuard`	`TestFormalVAL_P4_ForkProtectionRepoIDComparison`	PR workflows contain head.repo.id == repository_id guard (PM-08)
`VAL-P5 RBACPreActivationGates`	`TestFormalVAL_P5_PreActivationGatesActivation`	pre_activation gates activation via membership check (PM-10/PM-11)
`VAL-P6 ThreatDetectionOrdering`	`TestFormalVAL_P6_DetectionJobBetweenAgentAndSafeOutputs`	detection sits between agent and safe_outputs (TD-01)
`VAL-P7 ActionPinningSHA40`	`TestFormalVAL_P7_ActionPinsAre40CharSHA`	all non-local uses: pinned to 40-char SHA (CS-10)
`VAL-P8 TimestampValidationStep`	`TestFormalVAL_P8_ActivationContainsTimestampCheck`	activation references check_workflow_timestamp (RS-01/RS-02)
`VAL-P9 ConcurrencyDynamicGroup`	`TestFormalVAL_P9_ConcurrencyGroupContainsDynamicExpr`	concurrency.group contains dynamic ${{ }} expression (RS-16/RS-17)
`VAL-P10 PermissionWriteOnlySafeOutput`	`TestFormalVAL_P10_WritePermissionsIsolatedToSafeOutputs`	activation/agent have no write permissions (OI-07)
`VAL-P11 ConcurrencyQueueConflict`	`TestFormalVAL_P11_QueueMaxConflictsWithCancelInProgress`	queue:max + cancel-in-progress:true rejected (RS-22)
`VAL-P12 SanitizationRunStepExpr`	`TestFormalVAL_P12_RunStepExpressionsExtractedToEnv`	table-driven edge cases: empty, no-expr, multi-expr (IS-04)
`VAL-P13 EmptyGroupExpressionRejected`	`TestFormalVAL_P13_EmptyConcurrencyGroupRejected`	empty/whitespace concurrency group rejected (RS-17)
`VAL-P14 MalformedGroupExprRejected`	`TestFormalVAL_P14_MalformedConcurrencyExprRejected`	unbalanced ${{ }} in concurrency group rejected (RS-17)
`VAL-P15 WritePolicyRejectedInStrict`	`TestFormalVAL_P15_WritePermissionsRejectedInStrictMode`	strict-mode compiled activation/agent have no write perms (PM-01)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[formal-spec] security-architecture-spec-validation.md — Formal model & test suite — 2026-07-18 #46456

Summary

Specification

Formal Model

Behavioral Coverage Map

Generated Test Suite

Usage

Context

Metadata

Assignees

Labels

Type

Fields

Projects

Milestone

Relationships

Development

Uh oh!

[formal-spec] security-architecture-spec-validation.md — Formal model & test suite — 2026-07-18 #46456

Description

Summary

Specification

Formal Model

Behavioral Coverage Map

Generated Test Suite

Usage

Context

Metadata

Metadata

Assignees

Labels

Type

Fields

Projects

Milestone

Relationships

Development

Issue actions