feat(firmware): validate configuration and migrate sensor-driven flight APIs

Validate configuration through its owning schemas and keep board
declarations separate from shared F722 resource ownership. Bound USB
transitions, isolate transport failures and retain restart-only activation.

Migrate navigation and flight consumers with the sensor and schema
contracts. Require explicit installation data and synchronous output
authority; board motor outputs remain inhibited.

Validation: assembled-prefix host tests, strict Clippy, platform/USB tests
and both ARM release builds. Final-source coverage and scoped Miri/Kani
evidence are retained separately from hardware qualification.

firmware/libs/kaptan-control/src/kani_proofs.rs

@@ -0,0 +1,95 @@
+//! Constructor and one-step inductive PID invariants over all f32 bit patterns.
+
+use super::{MAXIMUM_CONTROL_STEP_SECONDS, Pid, PidConfig, PidError};
+
+fn any_config() -> PidConfig {
+    PidConfig {
+        proportional: f32::from_bits(kani::any()),
+        integral: f32::from_bits(kani::any()),
+        derivative: f32::from_bits(kani::any()),
+        output_limit: f32::from_bits(kani::any()),
+        integral_limit: f32::from_bits(kani::any()),
+    }
+}
+
+fn bits(pid: Pid) -> [u32; 6] {
+    [
+        pid.config.proportional.to_bits(),
+        pid.config.integral.to_bits(),
+        pid.config.derivative.to_bits(),
+        pid.config.output_limit.to_bits(),
+        pid.config.integral_limit.to_bits(),
+        pid.integral_contribution.to_bits(),
+    ]
+}
+
+#[kani::proof]
+// The generated equality check compares up to 24 bytes through memcmp.
+#[kani::unwind(25)]
+fn pid_constructor_establishes_invariant() {
+    let config = any_config();
+    let result = Pid::new(config);
+    let valid_gains = [config.proportional, config.integral, config.derivative]
+        .into_iter()
+        .all(|gain| gain.is_finite() && gain >= 0.0);
+    let valid_limits = config.output_limit.is_finite()
+        && config.output_limit > 0.0
+        && config.integral_limit.is_finite()
+        && config.integral_limit >= 0.0;
+
+    assert_eq!(result.is_ok(), valid_gains && valid_limits);
+    if let Ok(pid) = result {
+        assert_eq!(pid.integral_contribution.to_bits(), 0.0_f32.to_bits());
+        // Replace the returned configuration with the original input to check
+        // exact preservation, including the sign of zero-valued gains.
+        assert_eq!(bits(pid)[..5], bits(Pid { config, ..pid })[..5]);
+    }
+    kani::cover!(result.is_ok());
+    kani::cover!(result.is_err());
+    kani::cover!(config.proportional.is_nan());
+}
+
+#[kani::proof]
+#[kani::unwind(25)]
+fn pid_update_preserves_bounds_or_state() {
+    let Ok(mut pid) = Pid::new(any_config()) else {
+        return;
+    };
+
+    // The constructor establishes zero. This step permits every finite retained
+    // integral within its limit, a superset of all reachable PID histories.
+    let initial = f32::from_bits(kani::any());
+    kani::assume(initial.is_finite());
+    kani::assume(initial.abs() <= pid.config.integral_limit);
+    pid.integral_contribution = initial;
+    let before = bits(pid);
+
+    let error = f32::from_bits(kani::any());
+    let error_rate = f32::from_bits(kani::any());
+    let dt_seconds = f32::from_bits(kani::any());
+    let result = pid.update(error, error_rate, dt_seconds);
+
+    if let Ok(output) = result {
+        assert!(output.is_finite());
+        assert!(output.abs() <= pid.config.output_limit);
+        assert!(pid.integral_contribution.is_finite());
+        assert!(pid.integral_contribution.abs() <= pid.config.integral_limit);
+        assert_eq!(bits(pid)[..5], before[..5]);
+    } else {
+        assert_eq!(bits(pid), before);
+    }
+    kani::cover!(result.is_ok() && pid.integral_contribution != initial);
+    kani::cover!(result.is_ok_and(|output| output.abs() == pid.config.output_limit));
+    kani::cover!(
+        result == Err(PidError::NonFinite)
+            && error.is_finite()
+            && error_rate.is_finite()
+            && dt_seconds.is_finite()
+            && dt_seconds > 0.0
+            && dt_seconds <= MAXIMUM_CONTROL_STEP_SECONDS
+    );
+
+    pid.reset();
+    assert_eq!(pid.integral_contribution.to_bits(), 0.0_f32.to_bits());
+    assert_eq!(bits(pid)[..5], before[..5]);
+}