Composition: Aerospace Flight Control (Waterfall + V-Model + Cleanroom + inline Formal Verification)

DO-178C flight-control software archetype: Waterfall system/software requirements capture, V-Model decomposition with per-level verification plans, Cleanroom incremental development with statistical usage testing, **inline** formal verification of critical properties (parallel per-property proofs with **executed** proof-checker output), certification evidence assembly behind an independent adversarial certification gate, and a policy-gated flight-software baseline release. Every stage exit is guarded by an **executed** requirement-to-verification traceability gate plus a routed verification-lead sign-off; safety-requirement waivers, DER certification sign-off, and baseline release are **fail-closed** policy-gated approvals that never auto-execute.

Implements library/methodologies/backlog.md Example 6 (line 2183, previously *Not Implemented*). Pairs with composition-regulated-greenfield to complete the **safety / compliance quadrant** of the methodology matrix.

Why this composition

Each ingredient contributes a distinct DO-178C capability:

certification authorities audit (system/software requirements capture).

test level, making requirement-to-verification traceability *computable* and giving each level its own DO-178C verification plan (independence + structural coverage objectives).

and statistical certification of reliability over an operational usage model.

(safety invariants, control-loop timing/liveness, numerical stability) that testing alone cannot certify to Level A confidence.

• **Waterfall** — staged rigor and the frozen, sign-off-gated document sequence
• **V-Model** — every left-side design artifact is paired with its right-side
• **Cleanroom** — defect prevention through box-structure formal specification
• **Formal Verification** — machine-checkable proofs for the critical properties

Inline formal verification (missing-ingredient rationale)

There is **no** library/methodologies/formal-verification/ directory in the library. Rather than reference a nonexistent dir or skip the ingredient, the formal-verification methodology is modeled **inline** as first-class caf.formal-* tasks inside this composition, following the **batch-3 strangler-fig precedent** established by composition-legacy-modernization (which models legacy-modernization strangler-fig behavior inline the same way).

The inline seam is deliberately extraction-ready. A future standalone formal-verification methodology dir can lift, unchanged:

-> caf.property-proof (executed) -> caf.fix-formal (counterexample-driven),

artifacts/caf/formal/<propertyId>/proof-output.json {propertyId, proofStatus, executionRecord{statesExplored|obligationsDischarged, bound, wallTime}, counterexample|null}.

• the task set caf.formal-property-extraction -> caf.formal-model-construction
• the caf.formal.proof-audit adversarial gate, and
• the **proof-evidence schema**

This kip fact records the seam: process:composition-aerospace-flight-control --inlines-methodology--> methodology:formal-verification with props.seam = 'caf.formal-* task set + proof-evidence schema'.

Phase flow

Phases are strictly sequential. ctx.parallel.all is used only **within** a phase:

• **Phase 2** — per-level verification planning (four V-Model levels) and per-module module design.
• **Phase 4** — per-property formal analysis (model construction -> executed proof -> bounded fix).
• **Phase 5** — per-module (unit) and per-suite (integration) work; the four verification **levels** are sequential.
• **Phase 3** increments are deliberately **sequential** — Cleanroom increments build on prior increments.

Ingredients composed by name

Ingredient process() functions are **not** called — only exported defineTask tasks are composed, so ingredient-internal breakpoints/loops never double-fire.

Combinators (routedBreakpoint, adversarialGate, kipRecall, kipAssert) are imported from ../../specializations/common-utilities/routed-gate-combinators.js — never re-implemented.

Local caf.* tasks (all kind: 'agent'): caf.safety-assessment, caf.level-verification-plan, caf.trace-diff, caf.formal-property-extraction, caf.formal-model-construction, caf.property-proof, caf.fix-formal, caf.fix-verification, caf.assemble-certification-evidence, caf.baseline-release.

Task-registry collision

waterfall.js and v-model.js both register the task id implementation at module-evaluation time (a known library-wide shared-id issue). This composition uses **neither** module's implementation task — Cleanroom's implementIncrementTask does implementation — so the two modules are imported sequentially via top-level await import(...), and the inert colliding definition is cleared between them (the same pattern as composition-regulated-greenfield).

Policy-gated actions (adapters/policy ready)

breakpointId === actionId exactly; none carries autoApproveAfterN or presentAlwaysApprove; every decision records autoApproved: false provenance.

**Process breakpoints** (not policy-gated actions): caf.stage-exit.<stage> (verification-lead, one per stage exit: requirements, decomposition, cleanroom-development, formal-verification, verification) and failure-only owner escalations (caf.phase-3.design-escalation.<increment>, caf.phase-3.inspection-escalation.<increment>, caf.phase-5.<level>-escalation.<scope>). Owner acceptance of a shortfall touching a safety requirement **additionally** requires requirement-waiver-approval — owner escalation never substitutes for the certification-liaison waiver.

Stage-exit contract (`certifiedStageExit`)

1. **Executed traceability** — traceabilityMatrixTask computes the stage matrix; caf.trace-diff diffs it against the previous stored matrix + the SRS requirement set, writing artifacts/caf/<stage>/trace-diff.json. 2. **Adversarial gate** — adversarialGate (gateId: caf.<stage>.traceability) over the executed diff with traceability-critic + waiver-provenance-critic, IRON LAW ("re-run the trace computation or cite the executed trace-diff.json line-by-line"), bounded fixer, owner escalation. Gate failure throws. 3. **verification-lead sign-off** — routedBreakpoint with the per-stage-unique caf.stage-exit.<stage> id; payload built from the executed gate result after a structural malformed-check, so sign-off without traceability evidence is impossible to construct. 4. **Rejected sign-off throws** — stages are sequential, no skip-ahead.

Gate catalog and evidence schemas

The certification gate is **independent and adversarial**: certification-auditor + evidence-integrity-critic are distinct from all producer roles **and** from every per-stage critic; the auditor must SPOT-CHECK by re-executing at least one test level and one property proof and diffing against recorded outputs. Every gate reviews **executed** artifacts — never prose.

Inputs

Outputs

{ success, srs, safetyAssessment, vModelDesign, cleanroomDevelopment, formalVerification, verification, traceabilityMatrices, waivers, certificationEvidence, signoffs, baselineRelease, metadata }

flight-software-baseline-release breakpoint is rejected — no fallback path.

acceptance) plus levelGates.

records {breakpointEventId, breakpointId, requirementIds, rationale, requestingStage, approvedAt, respondedBy, autoApproved:false}.

• baselineRelease is null and success is false whenever the
• verification is keyed by level (unit / integration / system /
• waivers is the full safety-requirement waiver provenance log; each entry

Exported tasks and helpers

Usage

babysitter run:create \
  --process library/methodologies/composition-aerospace-flight-control/composition-aerospace-flight-control.js \
  --input '{"systemRequirements": "Fly-by-wire primary flight control: pitch/roll/yaw command laws with triple-redundant actuators, envelope protection, and a 20ms control-loop deadline. DO-178C Level A.", "flightControlFunctions": ["pitch-law", "roll-law", "envelope-protection"], "criticalPropertiesHint": ["actuator-command-bounds", "control-loop-deadline", "mode-exclusion"]}'

Relationship to ingredients and to composition-regulated-greenfield

This composition and composition-regulated-greenfield together fill the safety/compliance quadrant. composition-regulated-greenfield targets a HIPAA-regulated greenfield build (Waterfall + DDD + Cleanroom + V-Model with PHI-access policy gating); this one targets a DO-178C flight-control build, swapping DDD for **inline formal verification** and adding the certification evidence package + baseline release. Both share the same backbone: combinator-based routed breakpoints and adversarial gates, an executed-trace stage-exit contract, guarded policy-gated executors, per-item waiver/approval provenance threading, and kip recall/assert (here under kind methodology-composition). The caf.formal-* seam documented above is the extraction point should formal verification become a standalone methodology dir.