[formal-spec] awf-config-sources-spec.md — Formal model & test suite — 2026-06-08

[github-actions]

Summary

awf-config-sources-spec.md defines a conformance protocol for AWF configuration canonicalization. Agents and schema-reconciliation workflows must consult both docs/awf-config-spec.md (normative spec) and docs/awf-config.schema.json (published schema) from github/gh-aw-firewall before generating or validating AWF config behavior. The spec introduces the DriftRecord entity, a 5-business-day remediation SLA with escalation requirements (CR-06/CR-06a), and degraded-mode safeguards when canonical sources are temporarily unavailable. Ten formal predicates were derived from the conformance requirements and encoded as a Go testify suite.

Specification

• File: specs/awf-config-sources-spec.md
• Focus area: AWF config canonical source conformance, schema drift detection, SLA enforcement, degraded-mode safeguards
• Formal notation used: TLA+ (state machines, temporal properties), F* (pre/post contracts), Z3/SMT-LIB (enum constraints)

Formal Model

Predicates and invariants (illustrative notation)

P1 — DualSourceConsultation (CR-01) — TLA+

ValidSession(s) => s.specConsulted ∧ s.schemaConsulted
Both docs/awf-config-spec.md and docs/awf-config.schema.json must be loaded; consulting one source alone is insufficient.

P2 — NoUndocumentedFieldGeneration (CR-03) — Z3

may_generate(f) => f ∈ NormativeSpec ∨ f ∈ AnySchema
Agents MUST NOT emit config fields absent from both normative spec and all JSON schemas.

P3 — DriftRecordStructuralValidity (§4.5.1) — F*

All four required fields (property_path, drift_category, suggested_action, detected_at) must be non-empty/non-zero.

P4 — DriftCategoryExhaustiveness (§4.5.1) — Z3 enum

drift_category ∈ {missing_in_ghaw, missing_in_schema, spec_mismatch} — any other value is invalid.

P5 — SchemaOnlyPropertyFlaggedAsDrift (CR-02) — TLA+

p ∈ SchemaProperties ∧ ¬InGhAW(p) => ∃ r ∈ DriftReport: r.property_path = p ∧ r.drift_category = missing_in_ghaw

P6 — CorrectionPRForActionableDrift (CR-05/§4.2) — F*

r.drift_category ∈ {missing_in_ghaw, spec_mismatch} => corrective_pr_opened

P7 — SLARemediationWindow (CR-06) — TLA+ temporal

now > AddBusinessDays(d.detected_at, 5) => d.remediated ∨ EscalationIssueOpened(d)

P8 — EscalationIssueStructure (CR-06a) — F* record

∀ e: EscalationIssue. valid(e) <=> e.owner ≠ "" ∧ |e.unblock_plan| > 0 ∧ e.revised_eta ≠ zero

P9 — SafeguardDegradedModeOnUnavailability (§5) — TLA+

CanonicalUnavailable => UseLastSnapshot ∧ EmitWarning ∧ ¬PerformDestructiveOps

P10 — DriftReportEmittedOnDetection (§4.2 step 5) — F* postcondition

run_drift_detection(props) : []DriftRecord — always returns non-nil slice; each record satisfies P3.

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
DualSourceConsultation (CR-01)	TestFormal_P1_DualSourceConsultation	Both normative spec and JSON schema consulted; single-source sessions rejected
NoUndocumentedFieldGeneration (CR-03)	TestFormal_P2_NoUndocumentedFieldGeneration	Known-good fields allowed; unknown fields rejected
DriftRecordStructuralValidity (§4.5.1)	TestFormal_P3_DriftRecordStructuralValidity	All four required fields must be non-empty; any missing field invalidates the record
DriftCategoryExhaustiveness (§4.5.1)	TestFormal_P4_DriftCategoryExhaustiveness	Exactly three valid enum values; typos and unknowns rejected
SchemaOnlyPropertyFlaggedAsDrift (CR-02)	TestFormal_P5_SchemaOnlyPropertyFlaggedAsDrift	Uncovered schema properties (CLI or config-only) must produce drift records
CorrectionPRForActionableDrift (CR-05)	TestFormal_P6_CorrectionPRForActionableDrift	missing_in_ghaw and spec_mismatch require a corrective PR; missing_in_schema does not
SLARemediationWindow (CR-06)	TestFormal_P7_SLARemediationWindow	Business-day arithmetic correct; 5-day window enforced; weekends skipped
EscalationIssueStructure (CR-06a)	TestFormal_P8_EscalationIssueStructure	Valid only with owner, unblock plan, and non-zero revised ETA
SafeguardDegradedModeOnUnavailability (§5)	TestFormal_P9_SafeguardDegradedModeOnUnavailability	Unavailable sources trigger snapshot use, warning, destructive-op suppression
DriftReportEmittedOnDetection (§4.2)	TestFormal_P10_DriftReportEmittedOnDetection	Detection always produces non-nil slice; uncovered → records; covered → omitted

Generated Test Suite

📄 `pkg/workflow/awf_config_drift_formal_test.go` — 623 lines, 10 test functions, 39 sub-cases

Key types (stubs — replace with real implementation):

(go/redacted):build !integration

// Spec: specs/awf-config-sources-spec.md  Predicates: P1–P10 (see comment block in full file)
package workflow_test

import ("testing"; "time"; "github.com/stretchr/testify/assert"; "github.com/stretchr/testify/require")

type DriftCategory string
const (
    DriftCategoryMissingInGhAW   DriftCategory = "missing_in_ghaw"
    DriftCategoryMissingInSchema DriftCategory = "missing_in_schema"
    DriftCategorySpecMismatch    DriftCategory = "spec_mismatch"
)
type DriftRecord struct {
    PropertyPath string; DriftCategory DriftCategory
    SuggestedAction string; DetectedAt time.Time
}
type CanonicalSources struct{ SpecConsulted, SchemaConsulted bool }
func (c CanonicalSources) BothConsulted() bool { return c.SpecConsulted && c.SchemaConsulted }
type EscalationIssue struct {
    Owner string; UnblockPlan []string; RevisedETA, DetectedAt time.Time; RunURL string
}
func (e EscalationIssue) IsValid() bool {
    return e.Owner != "" && len(e.UnblockPlan) > 0 && !e.RevisedETA.IsZero()
}
type DegradedModeDecision struct {
    UsedSnapshot, SkippedDestructive, EmittedWarning bool; FailedSourcePaths []string
}

Example test — P1 (CR-01 dual-source enforcement):

func TestFormal_P1_DualSourceConsultation(t *testing.T) {
    cases := []struct{ name string; sources CanonicalSources; wantValid bool }{
        {"both consulted — valid", CanonicalSources{true, true}, true},
        {"only spec — insufficient", CanonicalSources{true, false}, false},
        {"only schema — insufficient", CanonicalSources{false, true}, false},
        {"neither — insufficient", CanonicalSources{false, false}, false},
    }
    for _, tc := range cases {
        t.Run(tc.name, func(t *testing.T) {
            assert.Equal(t, tc.wantValid, tc.sources.BothConsulted(),
                "CR-01: both docs/awf-config-spec.md and docs/awf-config.schema.json must be consulted")
        })
    }
}

Example test — P7 (CR-06 SLA business-day window):

func TestFormal_P7_SLARemediationWindow(t *testing.T) {
    t.Run("5 biz days from Mon 2026-06-08 → Mon 2026-06-15", func(t *testing.T) {
        assert.Equal(t, time.Date(2026,6,15,0,0,0,0,time.UTC),
            addBusinessDays(time.Date(2026,6,8,0,0,0,0,time.UTC), 5),
            "CR-06: SLA deadline arithmetic must be correct")
    })
    t.Run("7 biz days after detection — SLA exceeded", func(t *testing.T) {
        detected := time.Date(2026,6,1,10,0,0,0,time.UTC)
        now := time.Date(2026,6,10,10,0,0,0,time.UTC)
        assert.False(t, now.Before(addBusinessDays(detected, 5)),
            "CR-06: escalation issue MUST be opened when SLA exceeded")
    })
}

Full test file (623 lines) available at the path above. All 10 test functions follow the same table-driven pattern and cover P1–P10.

Usage

1. Copy full test file to pkg/workflow/awf_config_drift_formal_test.go.
2. Replace // stub types with real implementations when available.
3. Run: go test ./pkg/workflow/... -run Formal

Context

• Spec processed: specs/awf-config-sources-spec.md
• Formal notation: TLA+ · F* · Z3/SMT-LIB
• Run: §27152576719

Warning

Firewall blocked 1 domain

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:

network:
  allowed:
    - defaults
    - "proxy.golang.org"

See Network Configuration for more information.

Generated by 🔬 Daily Formal Spec Verifier · ⌖ 29.8 AIC · ⊞ 19K · ◷

• expires on Jun 15, 2026, 8:58 AM UTC-08:00