coord: gale v0.5.0 CUT — the 0.5 safety track is verified (partition switch / HM-failsafe / MPU / timer)

artifacts/design-decisions.yaml

@@ -1260,9 +1260,24 @@ artifacts:
           `proposed` until its full oracle passes; there is NO cut v0.5.0 release yet (latest tag =
           v0.4.0). The safety-critical pieces jess's failsafe + partition actually need - the I-ISO MPU
           region-program core, the PARTITION-SWITCH FSM (REQ-PIX-004 / DD-025 ARINC-653), the value-
-          domain HM/FAILSAFE FSM (REQ-PIX-009) - live on that 0.5 safety track and are NOT yet released.
-          jess consumes the v0.4.0 msgq/gust:os now; the safety FSMs are a WATCH item (consume when gale
-          cuts v0.5.0+ with the VERs verified), NOT a current dependency to build against.
+          domain HM/FAILSAFE FSM (REQ-PIX-009) - live on that 0.5 safety track.
+          UPDATE 2026-07-24 - GALE v0.5.0 CUT: the 0.5 safety track is now RELEASED with its VERs
+          VERIFIED (no longer proposed): VER-OS-ISO-001 (I-ISO MPU region-swap hardware-isolation
+          boundary), VER-OS-SWITCH-001 (two-level partition switch = verified Switcher x verified MPU,
+          end-to-end qemu + multi-core Renode placement demo -> REQ-PIX-004/DD-025 ARINC-653),
+          VER-OS-HM-001 (Health-Monitor cross-sensor voting + per-cause failsafe demonstrator ->
+          REQ-PIX-009 F100 failsafe), VER-OS-TIMER-001 (tickless component sleep over the verified
+          executor), VER-OS-SYSCALL-001 (gust:os seam). Plus a spar/AADL board.SoC.device model +
+          `gust-target-gen` (emits per-target constants / memory.x / WIT worlds), SILICON-VALIDATED on
+          STM32F100 (jess's F100 gust core!) + STM32G474. So the safety FSMs jess's failsafe+partition
+          need are now DELIVERED+verified, not a watch item. STILL NOT SHIPPED as standalone assets: the
+          v0.5.0 release ships only msgq/mutex/sem .o (msgq still needs the ~9-symbol scheduler seam:
+          k_spin_lock/unlock, z_ready_thread, z_reschedule, z_unpend_first_thread, gale_w_msgq_pend/
+          thread_swap_data/memcpy, arch_thread_return_value_set) + the gust:os probes - the verified
+          FSMs/executor themselves aren't standalone linkable .o. So to CONSUME them jess still links the
+          fused gale-nano core (or asks gale to expose the seam) - the concrete gale ask to FILE when
+          jess can bind (#369/float-gated, not yet). gust-target-gen may reconcile with jess's own
+          hardware/pixhawk6x-rt.aadl (both model the F100) - a coordination item to check.
         - RELAY (falcon + relay-hal): PARTITION the stack along the core boundaries (flight
           / estimator / failsafe) so each is separately fuse+compilable; plus the DD-022
           driver asks (TF02 rangefinder REQ-PIX-020, dual-M9N blend, 4S AdcIn). Sequenced

artifacts/phase2-pixhawk.yaml

@@ -148,6 +148,12 @@ artifacts:
       campaign: NavState delayed 1-2 ticks / jittered +-1 must keep hover + rotor-out passing).
       Per-core compiles gated on the synth float poles (#719 f32 + f64 phase-2; note falcon-flight
       has 4 f64-dense funcs so M7 double-FP is a real dependency - AFD-024).
+      GALE v0.5.0 GROUNDING 2026-07-24 (DD-023): the ARINC-653 two-level partition (DD-025) now has a
+      VERIFIED gale substrate - VER-OS-SWITCH-001 (two-level partition switch = verified Switcher x
+      verified MPU, proven end-to-end on qemu + a multi-core Renode placement demo) + VER-OS-ISO-001
+      (I-ISO MPU region-swap as the hardware isolation boundary). So the partition-switch + memory-
+      isolation mechanism jess's 3-core partition needs is verified upstream; jess consumes it by
+      linking the fused gale-nano core per DD-023.
     fields:
       category: functional
       priority: should
@@ -298,6 +304,14 @@ artifacts:
       default); the Renode stm32f103 confirmation runs hermetically with no board write.
       Offered on gale#65. Caveat: F100 = Cortex-M3 = thumbv7m (no DSP/FPU) - confirm synth
       M3 path + recalibrate fuel->cycles (kiln R4).
+      GALE v0.5.0 GROUNDING 2026-07-24 (the 0.5 safety track CUT, DD-023): gale now ships the
+      VERIFIED failsafe substrate this requirement needs - VER-OS-HM-001 (Health-Monitor cross-sensor
+      voting + per-cause failsafe demonstrator) + VER-OS-TIMER-001 (tickless component sleep over the
+      verified executor) + VER-OS-SYSCALL-001 (gust:os seam), and a gust-target-gen spar/AADL model
+      SILICON-VALIDATED on the STM32F100 (VER-TARGET-IWDG-001, + ADC/Vrefint). So the F100 gale-nano
+      failsafe FSM is verified upstream; jess's rung is to fuse+run it on the F100/M3 (extends the gust
+      pass-through TEST-PIX-028) - consumed by linking the fused gale-nano core (the standalone
+      kernel-seam .o is not a release asset; see DD-023).
     fields:
       category: functional
       priority: could