diff --git a/artifacts/verification/FV-FALCON-ADRC-002.yaml b/artifacts/verification/FV-FALCON-ADRC-002.yaml index 0bbc268..2a16ece 100644 --- a/artifacts/verification/FV-FALCON-ADRC-002.yaml +++ b/artifacts/verification/FV-FALCON-ADRC-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-ADRC-002 type: sw-verification title: "Inner-loop cadence-robustness certification + command-filter primitive — Kani + proptest + flight falsification (v0.33)" - status: approved + status: verified description: > Verification of the v0.33 inner-loop robustness work in relay-adrc: diff --git a/artifacts/verification/FV-FALCON-ATMOS-001.yaml b/artifacts/verification/FV-FALCON-ATMOS-001.yaml index fdba405..9c1e381 100644 --- a/artifacts/verification/FV-FALCON-ATMOS-001.yaml +++ b/artifacts/verification/FV-FALCON-ATMOS-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-ATMOS-001 type: sw-verification title: "Air-density thrust lapse: altitude integral + service ceiling (v1.22.0)" - status: approved + status: verified description: > Verification of the v1.22.0 atmosphere / thrust-lapse layer (25 falcon-core tests pass, clippy clean, embedded builds), realism arc release 7: diff --git a/artifacts/verification/FV-FALCON-ATT-001.yaml b/artifacts/verification/FV-FALCON-ATT-001.yaml index 2f92f1d..10bebdb 100644 --- a/artifacts/verification/FV-FALCON-ATT-001.yaml +++ b/artifacts/verification/FV-FALCON-ATT-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-ATT-001 type: sw-verification title: "Unit + property tests for relay-att + cascade hover bench (v0.4)" - status: approved + status: verified description: > v0.4 verification of the attitude controller (`relay-att`) and the full ATT → RATE → MIX → plant cascade closed-loop bench. diff --git a/artifacts/verification/FV-FALCON-AVOID-001.yaml b/artifacts/verification/FV-FALCON-AVOID-001.yaml index eeef5b6..01fe3be 100644 --- a/artifacts/verification/FV-FALCON-AVOID-001.yaml +++ b/artifacts/verification/FV-FALCON-AVOID-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-AVOID-001 type: sw-verification title: "Reactive keep-out zone avoidance (v1.31.0)" - status: approved + status: verified description: > Verification of the v1.31.0 keep-out avoidance (falcon-core 34 tests, clippy clean, embedded builds): diff --git a/artifacts/verification/FV-FALCON-BARO-001.yaml b/artifacts/verification/FV-FALCON-BARO-001.yaml index 24ca0d5..033c018 100644 --- a/artifacts/verification/FV-FALCON-BARO-001.yaml +++ b/artifacts/verification/FV-FALCON-BARO-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-BARO-001 type: sw-verification title: "Barometer fusion holds altitude through GPS-vertical loss (v1.20.0)" - status: approved + status: verified description: > Verification of the v1.20.0 barometer-fusion layer (21 falcon-core tests pass, clippy clean), realism arc release 5: diff --git a/artifacts/verification/FV-FALCON-BAROMAGDRV-001.yaml b/artifacts/verification/FV-FALCON-BAROMAGDRV-001.yaml index af78e66..240dbac 100644 --- a/artifacts/verification/FV-FALCON-BAROMAGDRV-001.yaml +++ b/artifacts/verification/FV-FALCON-BAROMAGDRV-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-BAROMAGDRV-001 type: sw-verification title: "Mag (IST8310) + baro (BMP388) driver bodies — mock-bus tests + Kani (falcon v1.45)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-BAROMAGDRV-P01. The falcon-baromag crate (no_std/ no_alloc/forbid-unsafe) provides the IST8310 magnetometer and BMP388 diff --git a/artifacts/verification/FV-FALCON-BATTERY-001.yaml b/artifacts/verification/FV-FALCON-BATTERY-001.yaml index 4f66e31..8de89b4 100644 --- a/artifacts/verification/FV-FALCON-BATTERY-001.yaml +++ b/artifacts/verification/FV-FALCON-BATTERY-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-BATTERY-001 type: sw-verification title: "Low-battery failsafe on a real draining pack (v1.21.0)" - status: approved + status: verified description: > Verification of the v1.21.0 battery-drain layer (22 falcon-core tests pass, clippy clean, embedded builds), realism arc release 6 (energy realism): diff --git a/artifacts/verification/FV-FALCON-CALIB-001.yaml b/artifacts/verification/FV-FALCON-CALIB-001.yaml index 2587810..7ed8e5f 100644 --- a/artifacts/verification/FV-FALCON-CALIB-001.yaml +++ b/artifacts/verification/FV-FALCON-CALIB-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-CALIB-001 type: sw-verification title: "Sensor calibration — synthetic-recovery + Kani totality + estimator consumption (falcon v1.98)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-CALIB-P01. Three layers: diff --git a/artifacts/verification/FV-FALCON-CMDLONG-001.yaml b/artifacts/verification/FV-FALCON-CMDLONG-001.yaml index 15ea81b..e0030aa 100644 --- a/artifacts/verification/FV-FALCON-CMDLONG-001.yaml +++ b/artifacts/verification/FV-FALCON-CMDLONG-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-CMDLONG-001 type: sw-verification title: "MAVLink COMMAND_LONG codec + RTL builder — round-trip, CRC_EXTRA, length-rejection (v0.14.2 carrier)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-MAVLINK-P05 (the COMMAND_LONG message + RTL builder, added at v0.14.2 after the v0.1 codec that FV-FALCON-MAVLINK-001 covers). diff --git a/artifacts/verification/FV-FALCON-COV-004.yaml b/artifacts/verification/FV-FALCON-COV-004.yaml index c7b705c..3757fe8 100644 --- a/artifacts/verification/FV-FALCON-COV-004.yaml +++ b/artifacts/verification/FV-FALCON-COV-004.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-COV-004 type: sw-verification title: "Cascade witness MC/DC via wasmtime+WASI subprocess harness (v0.15.1)" - status: approved + status: verified description: > v0.15.1 closes the cascade-target witness coverage WASI gap recorded in FV-FALCON-COV-001 (v0.13) and confirmed in diff --git a/artifacts/verification/FV-FALCON-COV-005.yaml b/artifacts/verification/FV-FALCON-COV-005.yaml index 17193bc..5adfde7 100644 --- a/artifacts/verification/FV-FALCON-COV-005.yaml +++ b/artifacts/verification/FV-FALCON-COV-005.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-COV-005 type: sw-verification title: "witness harness improvements + bazel macro (v0.16.0)" - status: approved + status: verified description: > v0.16.0 lands two harness improvements that close v0.15.1's deferred items 1 + 3, plus an upstream-bug report for item 2. diff --git a/artifacts/verification/FV-FALCON-CPREV-001.yaml b/artifacts/verification/FV-FALCON-CPREV-001.yaml index 43b6b47..8d4bf46 100644 --- a/artifacts/verification/FV-FALCON-CPREV-001.yaml +++ b/artifacts/verification/FV-FALCON-CPREV-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-CPREV-001 type: sw-verification title: "Collision prevention + precision landing — relay-avoid tests + Kani (falcon v1.44)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-CPREV-P01. The relay-avoid crate (no_std/no_alloc/ forbid-unsafe) provides the collision-prevention velocity limiter diff --git a/artifacts/verification/FV-FALCON-DC-001.yaml b/artifacts/verification/FV-FALCON-DC-001.yaml index 39cf71e..719de97 100644 --- a/artifacts/verification/FV-FALCON-DC-001.yaml +++ b/artifacts/verification/FV-FALCON-DC-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-DC-001 type: sw-verification title: "DroneCAN v0 transfer layer — relay-dronecan tests + Kani buffer-bound/totality proofs (DC-P01, v1.92)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-DC-P01. The relay-dronecan crate (no_std/no_alloc/ forbid-unsafe) implements the DroneCAN v0 transfer layer. Test-level diff --git a/artifacts/verification/FV-FALCON-DC-002.yaml b/artifacts/verification/FV-FALCON-DC-002.yaml index 71edd45..10095cd 100644 --- a/artifacts/verification/FV-FALCON-DC-002.yaml +++ b/artifacts/verification/FV-FALCON-DC-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-DC-002 type: sw-verification title: "DroneCAN ESC control path — NodeStatus/RawCommand codecs + single-frame TX, Kani-bounded (DC-P02, v1.93)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-DC-P02. relay-dronecan gains the ESC-path message codecs (msg.rs) and the single-frame transfer encoder (transfer.rs). diff --git a/artifacts/verification/FV-FALCON-DC-003.yaml b/artifacts/verification/FV-FALCON-DC-003.yaml index 8a234c0..60552ac 100644 --- a/artifacts/verification/FV-FALCON-DC-003.yaml +++ b/artifacts/verification/FV-FALCON-DC-003.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-DC-003 type: sw-verification title: "DroneCAN sensor ingest — float16 + esc.Status/mag/baro/battery decoders, Kani read_bits bound (DC-P03, v1.94)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-DC-P03. relay-dronecan gains the float16 primitive (float16.rs) and the sensor-ingest decoders (sensors.rs). Test-level diff --git a/artifacts/verification/FV-FALCON-DC-004.yaml b/artifacts/verification/FV-FALCON-DC-004.yaml index 447b309..0aec036 100644 --- a/artifacts/verification/FV-FALCON-DC-004.yaml +++ b/artifacts/verification/FV-FALCON-DC-004.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-DC-004 type: sw-verification title: "DroneCanNode async pump + NodeStatus heartbeat — sync/async equivalence + round-trip (DC-P04, v1.95)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-DC-P04. relay-dronecan gains the node runtime (node.rs) and the heartbeat encoder (msg.rs encode_node_status). diff --git a/artifacts/verification/FV-FALCON-DC-CONFORMANCE.yaml b/artifacts/verification/FV-FALCON-DC-CONFORMANCE.yaml index 9e47460..38e58ea 100644 --- a/artifacts/verification/FV-FALCON-DC-CONFORMANCE.yaml +++ b/artifacts/verification/FV-FALCON-DC-CONFORMANCE.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-DC-CONFORMANCE type: sw-verification title: "DroneCAN wire conformance — pydronecan reference-vector validation (fixes the DSDL bit-order bug)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-DC-P02 + SWREQ-FALCON-DC-P03 along the CONFORMANCE axis (does the decode match the real DSDL?), which the prior FV-FALCON-DC-002 diff --git a/artifacts/verification/FV-FALCON-DRAG-001.yaml b/artifacts/verification/FV-FALCON-DRAG-001.yaml index e0bb2ac..05791bc 100644 --- a/artifacts/verification/FV-FALCON-DRAG-001.yaml +++ b/artifacts/verification/FV-FALCON-DRAG-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-DRAG-001 type: sw-verification title: "Quadratic aerodynamic drag: tracking + damping (v1.17.0)" - status: approved + status: verified description: > Verification of the v1.17.0 aerodynamic-drag layer (17 falcon-core tests pass, clippy clean), realism arc release 2: diff --git a/artifacts/verification/FV-FALCON-EKF-001.yaml b/artifacts/verification/FV-FALCON-EKF-001.yaml index a5c9c81..6c786a0 100644 --- a/artifacts/verification/FV-FALCON-EKF-001.yaml +++ b/artifacts/verification/FV-FALCON-EKF-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-EKF-001 type: sw-verification title: "Unit + property tests + accuracy bench for relay-ekf (v0.2)" - status: approved + status: verified description: > v0.2 verification of the real Mahony complementary-filter attitude estimator (`relay-ekf`). Replaces the v0.1 stub diff --git a/artifacts/verification/FV-FALCON-EKF-002.yaml b/artifacts/verification/FV-FALCON-EKF-002.yaml index 9571338..4bf920d 100644 --- a/artifacts/verification/FV-FALCON-EKF-002.yaml +++ b/artifacts/verification/FV-FALCON-EKF-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-EKF-002 type: sw-verification title: "Adaptive IEKF process noise — Kani bound + mechanism test + decisive real-gz ANEES A/B (v0.35)" - status: approved + status: verified description: > Verification of the v0.35 motion-adaptive process-noise inflation: diff --git a/artifacts/verification/FV-FALCON-EKF-STUB-001.yaml b/artifacts/verification/FV-FALCON-EKF-STUB-001.yaml index c70393b..03c5fc8 100644 --- a/artifacts/verification/FV-FALCON-EKF-STUB-001.yaml +++ b/artifacts/verification/FV-FALCON-EKF-STUB-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-EKF-STUB-001 type: sw-verification title: "Unit + property tests for relay-ekf-stub (v0.1)" - status: approved + status: verified description: > Cargo unit + proptest verification of the relay-ekf-stub placeholder state estimator. Covers the v0.1 surrogate for diff --git a/artifacts/verification/FV-FALCON-ESCDRV-001.yaml b/artifacts/verification/FV-FALCON-ESCDRV-001.yaml index 90b667e..c0a95b1 100644 --- a/artifacts/verification/FV-FALCON-ESCDRV-001.yaml +++ b/artifacts/verification/FV-FALCON-ESCDRV-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-ESCDRV-001 type: sw-verification title: "ESC DShot + battery driver — protocol tests + Kani (falcon v1.43)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-ESCDRV-P01. The falcon-esc-dshot crate (no_std/ no_alloc/forbid-unsafe) provides the DShot throttle encoder diff --git a/artifacts/verification/FV-FALCON-FAULT-001.yaml b/artifacts/verification/FV-FALCON-FAULT-001.yaml index cce016a..a572b94 100644 --- a/artifacts/verification/FV-FALCON-FAULT-001.yaml +++ b/artifacts/verification/FV-FALCON-FAULT-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-FAULT-001 type: sw-verification title: "EKF-divergence watchdog — Verus + Kani + SITL fault-injection (v0.8 + v0.9.1)" - status: approved + status: verified description: > v0.8 verification of the EKF-divergence safety path: relay-hs EkfHealthMonitor + the falcon-sitl-hover `fault` diff --git a/artifacts/verification/FV-FALCON-FAULT-002.yaml b/artifacts/verification/FV-FALCON-FAULT-002.yaml index 7a4644e..4dbb71b 100644 --- a/artifacts/verification/FV-FALCON-FAULT-002.yaml +++ b/artifacts/verification/FV-FALCON-FAULT-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-FAULT-002 type: sw-verification title: "Single-rotor-loss fault tolerance — Kani MIX-P08 + FDI contract + reduced-attitude + end-to-end composition (v0.26)" - status: implemented + status: verified release: falcon-v1.103.0 description: > Three independently-verified components plus an end-to-end diff --git a/artifacts/verification/FV-FALCON-FAULT-003.yaml b/artifacts/verification/FV-FALCON-FAULT-003.yaml index 09a953a..6880bfd 100644 --- a/artifacts/verification/FV-FALCON-FAULT-003.yaml +++ b/artifacts/verification/FV-FALCON-FAULT-003.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-FAULT-003 type: sw-verification title: "Single-rotor-out FULL-LOOP recovery — parasitic-free rank-3 allocation + production-core spin-descent oracle (v1.114)" - status: implemented + status: verified release: falcon-v1.114.0 description: > Strengthens FV-FALCON-FAULT-002. That artifact verified the diff --git a/artifacts/verification/FV-FALCON-FLOWRANGE-001.yaml b/artifacts/verification/FV-FALCON-FLOWRANGE-001.yaml index f6e0432..a7af63d 100644 --- a/artifacts/verification/FV-FALCON-FLOWRANGE-001.yaml +++ b/artifacts/verification/FV-FALCON-FLOWRANGE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-FLOWRANGE-001 type: sw-verification title: "Rangefinder + optical-flow preprocessing — relay-flowrange tests + Kani (falcon v1.51)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-FLOWRANGE-P01. The relay-flowrange crate (no_std/ no_alloc/forbid-unsafe): range_to_altitude (tilt-compensated, band-gated) + diff --git a/artifacts/verification/FV-FALCON-FSAFE-001.yaml b/artifacts/verification/FV-FALCON-FSAFE-001.yaml index 3f561c2..02846f5 100644 --- a/artifacts/verification/FV-FALCON-FSAFE-001.yaml +++ b/artifacts/verification/FV-FALCON-FSAFE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-FSAFE-001 type: sw-verification title: "Failsafe arbiter — relay-fsafe tests + exhaustive Kani (falcon v1.41)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-FSAFE-P01. The relay-fsafe crate (no_std/no_alloc, forbid-unsafe) implements the FailsafeArbiter — the single prioritized diff --git a/artifacts/verification/FV-FALCON-FSM-001.yaml b/artifacts/verification/FV-FALCON-FSM-001.yaml index d6e3da2..e744634 100644 --- a/artifacts/verification/FV-FALCON-FSM-001.yaml +++ b/artifacts/verification/FV-FALCON-FSM-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-FSM-001 type: sw-verification title: "Flight-mode FSM — Kani disarm-safety + failsafe-recovery + lifecycle tests (v1.7.0)" - status: approved + status: verified description: > Verification of the v1.7.0 flight-mode state machine (relay-fsm): diff --git a/artifacts/verification/FV-FALCON-GEO-001.yaml b/artifacts/verification/FV-FALCON-GEO-001.yaml index d0677ef..d8db12d 100644 --- a/artifacts/verification/FV-FALCON-GEO-001.yaml +++ b/artifacts/verification/FV-FALCON-GEO-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-GEO-001 type: sw-verification title: "Geofence safety path — Verus proofs + SITL EW-spoof scenario (v0.10)" - status: approved + status: verified description: > v0.10 verification of the geofence safety path: the relay-lc Verus-verified Geofence engine + the falcon-sitl-hover diff --git a/artifacts/verification/FV-FALCON-GEO-002.yaml b/artifacts/verification/FV-FALCON-GEO-002.yaml index 3c48f94..52110f1 100644 --- a/artifacts/verification/FV-FALCON-GEO-002.yaml +++ b/artifacts/verification/FV-FALCON-GEO-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-GEO-002 type: sw-verification title: "Geofence::check — Kani bounded model checking (v0.11)" - status: approved + status: verified description: > v0.11 Kani harness pack on `relay_lc::engine::Geofence::check`. Mirrors the v0.9.1 pattern that pinned EkfHealthMonitor with diff --git a/artifacts/verification/FV-FALCON-GNDEFFECT-001.yaml b/artifacts/verification/FV-FALCON-GNDEFFECT-001.yaml index ebae7ff..abd0792 100644 --- a/artifacts/verification/FV-FALCON-GNDEFFECT-001.yaml +++ b/artifacts/verification/FV-FALCON-GNDEFFECT-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-GNDEFFECT-001 type: sw-verification title: "Ground effect: aids takeoff, documented landing float (v1.24.0)" - status: approved + status: verified description: > Verification of the v1.24.0 ground-effect layer (29 falcon-core tests pass, clippy clean, embedded builds), realism arc release 9: diff --git a/artifacts/verification/FV-FALCON-GNSS-001.yaml b/artifacts/verification/FV-FALCON-GNSS-001.yaml index aac8e96..36330ac 100644 --- a/artifacts/verification/FV-FALCON-GNSS-001.yaml +++ b/artifacts/verification/FV-FALCON-GNSS-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-GNSS-001 type: sw-verification title: "Noisy + intermittent GNSS: variance-matched hold vs over-trust divergence (v1.19.0)" - status: approved + status: verified description: > Verification of the v1.19.0 GNSS-realism layer (20 falcon-core tests pass, clippy clean), realism arc release 4: diff --git a/artifacts/verification/FV-FALCON-GNSSDRV-001.yaml b/artifacts/verification/FV-FALCON-GNSSDRV-001.yaml index 562df24..c793617 100644 --- a/artifacts/verification/FV-FALCON-GNSSDRV-001.yaml +++ b/artifacts/verification/FV-FALCON-GNSSDRV-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-GNSSDRV-001 type: sw-verification title: "GNSS UBX driver — protocol round-trip tests + Kani totality (falcon v1.42)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-GNSSDRV-P01. The falcon-gnss-ubx crate (no_std/ no_alloc/forbid-unsafe) implements UbxParser, a streaming UBX frame parser diff --git a/artifacts/verification/FV-FALCON-GZGE-001.yaml b/artifacts/verification/FV-FALCON-GZGE-001.yaml index 1bedde1..3817732 100644 --- a/artifacts/verification/FV-FALCON-GZGE-001.yaml +++ b/artifacts/verification/FV-FALCON-GZGE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-GZGE-001 type: sw-verification title: "Custom gz ground-effect plugin — cushion holds the vehicle aloft (v1.32.0)" - status: approved + status: verified description: > Verification of the v1.32.0 falcon GroundEffect gz-sim8 plugin. BENCH-ONLY: Gazebo is not in CI (the CI gate skips gz/meld/bazel steps), so this runs diff --git a/artifacts/verification/FV-FALCON-HAL-001.yaml b/artifacts/verification/FV-FALCON-HAL-001.yaml index cbfd1e0..b2b1170 100644 --- a/artifacts/verification/FV-FALCON-HAL-001.yaml +++ b/artifacts/verification/FV-FALCON-HAL-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-HAL-001 type: sw-verification title: "Backend-agnostic flight core — HAL seam + verified cascade stabilizes through it (v1.1.0)" - status: approved + status: verified description: > Verification of the v1.1.0 hardware-abstraction-layer seam (new crate falcon-core): diff --git a/artifacts/verification/FV-FALCON-HAL-002.yaml b/artifacts/verification/FV-FALCON-HAL-002.yaml index e913fc8..a6c5590 100644 --- a/artifacts/verification/FV-FALCON-HAL-002.yaml +++ b/artifacts/verification/FV-FALCON-HAL-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-HAL-002 type: sw-verification title: "Altitude hold + disturbance rejection through the HAL (v1.2.0)" - status: approved + status: verified description: > Verification of the v1.2.0 altitude/thrust loop + disturbance rejection in falcon-core (4 tests pass, clippy clean): diff --git a/artifacts/verification/FV-FALCON-HAL-003.yaml b/artifacts/verification/FV-FALCON-HAL-003.yaml index 5b5b5e2..d5f70f8 100644 --- a/artifacts/verification/FV-FALCON-HAL-003.yaml +++ b/artifacts/verification/FV-FALCON-HAL-003.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-HAL-003 type: sw-verification title: "Full 6-DoF position hold through the HAL — complete hover stack (v1.3.0)" - status: approved + status: verified description: > Verification of the v1.3.0 horizontal position loop in falcon-core (5 tests pass, clippy clean): diff --git a/artifacts/verification/FV-FALCON-HITL-001.yaml b/artifacts/verification/FV-FALCON-HITL-001.yaml index 897f583..618b5d7 100644 --- a/artifacts/verification/FV-FALCON-HITL-001.yaml +++ b/artifacts/verification/FV-FALCON-HITL-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-HITL-001 type: sw-verification title: "HITL RF-spoof harness — verdict contract + stub-backend regression (v0.11)" - status: approved + status: verified description: > v0.11 verification of the HITL harness that exercises the formally verified geofence safety path against an RF GPS diff --git a/artifacts/verification/FV-FALCON-HITL-002.yaml b/artifacts/verification/FV-FALCON-HITL-002.yaml index 6166f9f..2a71570 100644 --- a/artifacts/verification/FV-FALCON-HITL-002.yaml +++ b/artifacts/verification/FV-FALCON-HITL-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-HITL-002 type: sw-verification title: "HITL MavlinkBench — GLOBAL_POSITION_INT-driven backend (v0.12)" - status: approved + status: verified description: > v0.12 verification of the MavlinkBench backend that closes the live-FC telemetry gap recorded in FV-FALCON-HITL-001. diff --git a/artifacts/verification/FV-FALCON-HWSEAM-001.yaml b/artifacts/verification/FV-FALCON-HWSEAM-001.yaml index f825d34..669bbfa 100644 --- a/artifacts/verification/FV-FALCON-HWSEAM-001.yaml +++ b/artifacts/verification/FV-FALCON-HWSEAM-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-HWSEAM-001 type: sw-verification title: "Real-hardware backend seam composed end-to-end (v1.11.0)" - status: approved + status: verified description: > Verification of the v1.11.0 hardware seam (12 falcon-core tests pass, clippy clean, embedded Cortex-M crate still builds): diff --git a/artifacts/verification/FV-FALCON-IEKF-001.yaml b/artifacts/verification/FV-FALCON-IEKF-001.yaml index 8c79764..1e36fb2 100644 --- a/artifacts/verification/FV-FALCON-IEKF-001.yaml +++ b/artifacts/verification/FV-FALCON-IEKF-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-IEKF-001 type: sw-verification title: "IEKF SITL accuracy bench — full-state position/velocity tracking (falcon v1.38)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-IEKF-P01. The falcon-iekf-bench example exercises the verified relay-iekf full-state Invariant EKF over a deterministic 30 s diff --git a/artifacts/verification/FV-FALCON-IMUBIAS-001.yaml b/artifacts/verification/FV-FALCON-IMUBIAS-001.yaml index f587b9a..c2aca5a 100644 --- a/artifacts/verification/FV-FALCON-IMUBIAS-001.yaml +++ b/artifacts/verification/FV-FALCON-IMUBIAS-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-IMUBIAS-001 type: sw-verification title: "IEKF under random-walk gyro bias-instability (v1.18.0)" - status: approved + status: verified description: > Verification of the v1.18.0 IMU bias-instability layer (18 falcon-core tests pass, clippy clean), realism arc release 3 (first sensor-fidelity diff --git a/artifacts/verification/FV-FALCON-IMUDRV-001.yaml b/artifacts/verification/FV-FALCON-IMUDRV-001.yaml index 79e0943..5093b42 100644 --- a/artifacts/verification/FV-FALCON-IMUDRV-001.yaml +++ b/artifacts/verification/FV-FALCON-IMUDRV-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-IMUDRV-001 type: sw-verification title: "Reference ICM-42688 IMU driver: protocol + scaling against a mock bus (v1.13.0)" - status: approved + status: verified description: > Verification of the v1.13.0 falcon-imu-icm42688 driver (4 tests pass, clippy clean), the first concrete driver against the v1.11 ImuDriver seam: diff --git a/artifacts/verification/FV-FALCON-LINK-001.yaml b/artifacts/verification/FV-FALCON-LINK-001.yaml index 9bfb6c1..279341c 100644 --- a/artifacts/verification/FV-FALCON-LINK-001.yaml +++ b/artifacts/verification/FV-FALCON-LINK-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-LINK-001 type: sw-verification title: "HITL link backend: closed loop over the framed wire protocol (v1.14.0)" - status: approved + status: verified description: > Verification of the v1.14.0 falcon-hitl LinkBackend (2 tests pass, clippy clean), the third backend behind the HAL seam: diff --git a/artifacts/verification/FV-FALCON-LOG-001.yaml b/artifacts/verification/FV-FALCON-LOG-001.yaml index 03a798c..71ceca4 100644 --- a/artifacts/verification/FV-FALCON-LOG-001.yaml +++ b/artifacts/verification/FV-FALCON-LOG-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-LOG-001 type: sw-verification title: "Onboard flight logger — relay-log ring + replay tests + Kani (falcon v1.48)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-LOG-P01. The relay-log crate (no_std/no_alloc/ forbid-unsafe) is the bounded-ring black box: FlightLog + a 16-byte diff --git a/artifacts/verification/FV-FALCON-LYAP-001.yaml b/artifacts/verification/FV-FALCON-LYAP-001.yaml index e9688ac..7115403 100644 --- a/artifacts/verification/FV-FALCON-LYAP-001.yaml +++ b/artifacts/verification/FV-FALCON-LYAP-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-LYAP-001 type: sw-verification title: "Full-state Lyapunov — kernel-checked Lean position+combined proof + runnable certificate (v0.38)" - status: approved + status: verified description: > Verification of the v0.38 full-state Lyapunov certificate: diff --git a/artifacts/verification/FV-FALCON-MATHSEAM-001.yaml b/artifacts/verification/FV-FALCON-MATHSEAM-001.yaml index 5428cea..ba09ddb 100644 --- a/artifacts/verification/FV-FALCON-MATHSEAM-001.yaml +++ b/artifacts/verification/FV-FALCON-MATHSEAM-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MATHSEAM-001 type: sw-verification title: "Flight-math qualification seam: cascade migrated, faithful, builds (v1.12.0)" - status: approved + status: verified description: > Verification of the v1.12.0 relay-math qualification seam: diff --git a/artifacts/verification/FV-FALCON-MATHSEAM-002.yaml b/artifacts/verification/FV-FALCON-MATHSEAM-002.yaml index 8987aea..cb743b5 100644 --- a/artifacts/verification/FV-FALCON-MATHSEAM-002.yaml +++ b/artifacts/verification/FV-FALCON-MATHSEAM-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MATHSEAM-002 type: sw-verification title: "Flight-math seam extended to the remaining flight crates — seam now complete across the no_std flight path" - status: implemented + status: verified description: > FV-FALCON-MATHSEAM-001 migrated the v1.12 verified cascade (relay-iekf/geo/adrc/mix-quad/falcon-core) to the relay-math seam, but four diff --git a/artifacts/verification/FV-FALCON-MAVBRIDGE-001.yaml b/artifacts/verification/FV-FALCON-MAVBRIDGE-001.yaml index 399967b..cb84bce 100644 --- a/artifacts/verification/FV-FALCON-MAVBRIDGE-001.yaml +++ b/artifacts/verification/FV-FALCON-MAVBRIDGE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MAVBRIDGE-001 type: sw-verification title: "MAVLink ↔ flight-supervisor bridge — commands + telemetry (v1.28.0)" - status: approved + status: verified description: > Verification of the v1.28.0 falcon-mavlink bridge (11 unit tests pass, clippy clean, builds bare-metal for thumbv7em-none-eabihf). The bridge is diff --git a/artifacts/verification/FV-FALCON-MAVLINK-001.yaml b/artifacts/verification/FV-FALCON-MAVLINK-001.yaml index b16cd21..f67b654 100644 --- a/artifacts/verification/FV-FALCON-MAVLINK-001.yaml +++ b/artifacts/verification/FV-FALCON-MAVLINK-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MAVLINK-001 type: sw-verification title: "Unit + property tests for relay-mavlink (v0.1)" - status: approved + status: verified description: > Cargo unit + proptest verification of the relay-mavlink v2 codec. Covers the CRC-16/MCRF4XX algorithm, HEARTBEAT encode diff --git a/artifacts/verification/FV-FALCON-MISSION-001.yaml b/artifacts/verification/FV-FALCON-MISSION-001.yaml index 0d9f05d..fee2074 100644 --- a/artifacts/verification/FV-FALCON-MISSION-001.yaml +++ b/artifacts/verification/FV-FALCON-MISSION-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MISSION-001 type: sw-verification title: "Multi-waypoint mission sequencer + autonomous return (v1.30.0)" - status: approved + status: verified description: > Verification of the v1.30.0 mission sequencer (falcon-core 33 tests + relay-mavlink 55 + falcon-mavlink 11, clippy clean, embedded builds): diff --git a/artifacts/verification/FV-FALCON-MISSIONDL-001.yaml b/artifacts/verification/FV-FALCON-MISSIONDL-001.yaml index 379191d..187b252 100644 --- a/artifacts/verification/FV-FALCON-MISSIONDL-001.yaml +++ b/artifacts/verification/FV-FALCON-MISSIONDL-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MISSIONDL-001 type: sw-verification title: "MAVLink mission download — a GCS reads the mission back (v1.34.0)" - status: approved + status: verified description: > Verification of the v1.34.0 MAVLink mission-DOWNLOAD protocol (relay-mavlink 62 tests + falcon-mavlink 16, clippy clean, embedded builds): diff --git a/artifacts/verification/FV-FALCON-MISSIONUP-001.yaml b/artifacts/verification/FV-FALCON-MISSIONUP-001.yaml index 9cca1d3..49bd803 100644 --- a/artifacts/verification/FV-FALCON-MISSIONUP-001.yaml +++ b/artifacts/verification/FV-FALCON-MISSIONUP-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MISSIONUP-001 type: sw-verification title: "MAVLink mission upload — a GCS-defined mission flown end to end (v1.33.0)" - status: approved + status: verified description: > Verification of the v1.33.0 MAVLink mission-upload protocol (relay-mavlink 61 tests + falcon-mavlink 14, clippy clean, embedded builds): diff --git a/artifacts/verification/FV-FALCON-MIX-001.yaml b/artifacts/verification/FV-FALCON-MIX-001.yaml index 05cdc30..1d6eae8 100644 --- a/artifacts/verification/FV-FALCON-MIX-001.yaml +++ b/artifacts/verification/FV-FALCON-MIX-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MIX-001 type: sw-verification title: "Unit + property tests for relay-mix-quad (v0.4)" - status: approved + status: verified description: > v0.4 verification of the X-config quadcopter mixer (`relay-mix-quad`). Maps body-frame (torque, thrust) commands diff --git a/artifacts/verification/FV-FALCON-MIX-003.yaml b/artifacts/verification/FV-FALCON-MIX-003.yaml index 240b413..69294c0 100644 --- a/artifacts/verification/FV-FALCON-MIX-003.yaml +++ b/artifacts/verification/FV-FALCON-MIX-003.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MIX-003 type: sw-verification title: "Airframe-agnostic allocator — Kani unit-interval bound + quad-X bit-equivalence + hexa symmetry (v0.34)" - status: approved + status: verified description: > Verification of the v0.34 MixerN airframe-agnostic control allocator (relay-mix-quad): diff --git a/artifacts/verification/FV-FALCON-MIX-004.yaml b/artifacts/verification/FV-FALCON-MIX-004.yaml index 134a004..0ff42d3 100644 --- a/artifacts/verification/FV-FALCON-MIX-004.yaml +++ b/artifacts/verification/FV-FALCON-MIX-004.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MIX-004 type: sw-verification title: "Airframe-agnostic closed loop — hexa cascade stabilization (SITL) (v0.39)" - status: approved + status: verified description: > Verification of the v0.39 closed-loop "any drone" substantiation: diff --git a/artifacts/verification/FV-FALCON-MIXMULTI-001.yaml b/artifacts/verification/FV-FALCON-MIXMULTI-001.yaml index e8b6dbc..63cd161 100644 --- a/artifacts/verification/FV-FALCON-MIXMULTI-001.yaml +++ b/artifacts/verification/FV-FALCON-MIXMULTI-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MIXMULTI-001 type: sw-verification title: "Hex + coax mixers — relay-mix-multi tests + Kani (falcon v1.49)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-MIXMULTI-P01. The relay-mix-multi crate (no_std/ no_alloc/forbid-unsafe) provides hex_x (6) and octo_coax (8) N-rotor diff --git a/artifacts/verification/FV-FALCON-MODE-001.yaml b/artifacts/verification/FV-FALCON-MODE-001.yaml index 5a3a880..d110999 100644 --- a/artifacts/verification/FV-FALCON-MODE-001.yaml +++ b/artifacts/verification/FV-FALCON-MODE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MODE-001 type: sw-verification title: "Flight-mode sequence + position/altitude-hold bench (falcon v1.39)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-MODE-P01. falcon-hold-bench exercises the existing verified relay-fsm (flight-mode state machine) and relay-pos (position diff --git a/artifacts/verification/FV-FALCON-MODEXTRA-001.yaml b/artifacts/verification/FV-FALCON-MODEXTRA-001.yaml index 104de74..71df557 100644 --- a/artifacts/verification/FV-FALCON-MODEXTRA-001.yaml +++ b/artifacts/verification/FV-FALCON-MODEXTRA-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MODEXTRA-001 type: sw-verification title: "Extended flight modes — relay-modextra tests + Kani (falcon v1.52)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-MODEXTRA-P01. The relay-modextra crate (no_std/ no_alloc/forbid-unsafe): poi_yaw / follow_setpoint / land_in_place / diff --git a/artifacts/verification/FV-FALCON-MOTORDYN-001.yaml b/artifacts/verification/FV-FALCON-MOTORDYN-001.yaml index 6dd7cd1..87b93e4 100644 --- a/artifacts/verification/FV-FALCON-MOTORDYN-001.yaml +++ b/artifacts/verification/FV-FALCON-MOTORDYN-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-MOTORDYN-001 type: sw-verification title: "ADRC ESO absorbs first-order motor lag (v1.23.0)" - status: approved + status: verified description: > Verification of the v1.23.0 motor-dynamics layer (27 falcon-core tests pass, clippy clean, embedded builds), realism arc release 8 (a robustness diff --git a/artifacts/verification/FV-FALCON-NID-001.yaml b/artifacts/verification/FV-FALCON-NID-001.yaml index bb55a20..a97317d 100644 --- a/artifacts/verification/FV-FALCON-NID-001.yaml +++ b/artifacts/verification/FV-FALCON-NID-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-NID-001 type: sw-verification title: "Network ID codec — round-trip + fuzz + Kani + ASTM bit-packing for relay-nid (v0.9 + v0.9.1)" - status: approved + status: verified description: > v0.9 verification of the EASA U-space Network Identification codec (`crates/relay-nid`): diff --git a/artifacts/verification/FV-FALCON-NID-002.yaml b/artifacts/verification/FV-FALCON-NID-002.yaml index d91ba85..c0657bc 100644 --- a/artifacts/verification/FV-FALCON-NID-002.yaml +++ b/artifacts/verification/FV-FALCON-NID-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-NID-002 type: sw-verification title: "relay-nid — Verus dual-tree refactor + Option-totality contracts (v0.11)" - status: approved + status: verified description: > v0.11 brings relay-nid in line with the verified-engine pattern the rest of the workspace uses. Adds: diff --git a/artifacts/verification/FV-FALCON-OFFB-001.yaml b/artifacts/verification/FV-FALCON-OFFB-001.yaml index f48b450..3b339ce 100644 --- a/artifacts/verification/FV-FALCON-OFFB-001.yaml +++ b/artifacts/verification/FV-FALCON-OFFB-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-OFFB-001 type: sw-verification title: "Offboard setpoint-timeout failsafe — relay-offboard tests + Kani (falcon v1.40)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-OFFB-P01. The relay-offboard crate (no_std/no_alloc, forbid-unsafe) implements OffboardReceiver — the freshness/timeout state diff --git a/artifacts/verification/FV-FALCON-PACE-001.yaml b/artifacts/verification/FV-FALCON-PACE-001.yaml index e1a12b4..3e18ac3 100644 --- a/artifacts/verification/FV-FALCON-PACE-001.yaml +++ b/artifacts/verification/FV-FALCON-PACE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PACE-001 type: sw-verification title: "Gyro-synchronized loop pacing — pure-logic unit tests + A/B/C/D real-Gazebo load matrix (v0.32)" - status: approved + status: verified description: > Verification of the v0.32 two-stage gyro-synchronized loop scheduler: diff --git a/artifacts/verification/FV-FALCON-PARAM-001.yaml b/artifacts/verification/FV-FALCON-PARAM-001.yaml index 5fd48de..b7beaab 100644 --- a/artifacts/verification/FV-FALCON-PARAM-001.yaml +++ b/artifacts/verification/FV-FALCON-PARAM-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PARAM-001 type: sw-verification title: "Parameter store schema-bounded writes — relay-param tests + Kani (falcon v1.47)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-PARAM-P01. The relay-param crate (no_std/no_alloc/ forbid-unsafe) is the typed parameter store: register/get/set with diff --git a/artifacts/verification/FV-FALCON-PARAM-002.yaml b/artifacts/verification/FV-FALCON-PARAM-002.yaml index d63b49b..fb1fe04 100644 --- a/artifacts/verification/FV-FALCON-PARAM-002.yaml +++ b/artifacts/verification/FV-FALCON-PARAM-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PARAM-002 type: sw-verification title: "MAVLink PARAM binding — pymavlink wire conformance + bounded-store seam (falcon v1.96)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-PARAM-P02. Two layers, each independently checked: diff --git a/artifacts/verification/FV-FALCON-PATH-001.yaml b/artifacts/verification/FV-FALCON-PATH-001.yaml index ecd2106..b7ca5a2 100644 --- a/artifacts/verification/FV-FALCON-PATH-001.yaml +++ b/artifacts/verification/FV-FALCON-PATH-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PATH-001 type: sw-verification title: "Robustness under injected sensor pathologies through the HAL (v1.9.0)" - status: approved + status: verified description: > Verification of the v1.9.0 sensor-pathology robustness (11 falcon-core tests pass, clippy clean). The SimBackend gained a deterministic diff --git a/artifacts/verification/FV-FALCON-PERF-001.yaml b/artifacts/verification/FV-FALCON-PERF-001.yaml index 99c1af2..646bb41 100644 --- a/artifacts/verification/FV-FALCON-PERF-001.yaml +++ b/artifacts/verification/FV-FALCON-PERF-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PERF-001 type: sw-verification title: "per-engine throughput benchmarks — WCET-budget regression guard (#8)" - status: implemented + status: verified description: > Criterion per-cycle throughput benchmarks for the five core flight engines (LC / SCH / SC / HS / CFDP), guarding the Lean-proven WCET diff --git a/artifacts/verification/FV-FALCON-PIPELINE-001.yaml b/artifacts/verification/FV-FALCON-PIPELINE-001.yaml index 7cb9953..97b19ad 100644 --- a/artifacts/verification/FV-FALCON-PIPELINE-001.yaml +++ b/artifacts/verification/FV-FALCON-PIPELINE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PIPELINE-001 type: sw-verification title: "WASM pipeline — Component Model cascade under Bazel (v0.7)" - status: approved + status: verified description: > Verification of the falcon WASM pipeline. v0.6 built the control layer as raw `#[export_name]` scalar modules fused by meld; v0.7 diff --git a/artifacts/verification/FV-FALCON-POS-001.yaml b/artifacts/verification/FV-FALCON-POS-001.yaml index 6af41c3..369a025 100644 --- a/artifacts/verification/FV-FALCON-POS-001.yaml +++ b/artifacts/verification/FV-FALCON-POS-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-POS-001 type: sw-verification title: "Unit + property tests + mission SITL for relay-pos (v0.5)" - status: approved + status: verified description: > v0.5 verification of the position controller (`relay-pos`) and the full POS → ATT → RATE → MIX → plant cascade in the diff --git a/artifacts/verification/FV-FALCON-PREARM-001.yaml b/artifacts/verification/FV-FALCON-PREARM-001.yaml index 7dd4030..a2eb160 100644 --- a/artifacts/verification/FV-FALCON-PREARM-001.yaml +++ b/artifacts/verification/FV-FALCON-PREARM-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PREARM-001 type: sw-verification title: "Pre-arm entry gate — FSM-K03 + falcon-core seam (falcon v1.97)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-PREARM-P01: the FSM arm transition is gated on the pre-arm commander verdict, proven and wired end-to-end. diff --git a/artifacts/verification/FV-FALCON-PREARM-002.yaml b/artifacts/verification/FV-FALCON-PREARM-002.yaml index 46905b1..10bed26 100644 --- a/artifacts/verification/FV-FALCON-PREARM-002.yaml +++ b/artifacts/verification/FV-FALCON-PREARM-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PREARM-002 type: sw-verification title: "Pre-arm gate fed by real state — update_preflight + live-signal arming (falcon v1.99)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-PREARM-P02: the FlightSupervisor derives the pre-arm checks from real vehicle state each cycle, so the Kani-proven arm gate diff --git a/artifacts/verification/FV-FALCON-PREFLIGHT-001.yaml b/artifacts/verification/FV-FALCON-PREFLIGHT-001.yaml index aacdf8e..42a14c4 100644 --- a/artifacts/verification/FV-FALCON-PREFLIGHT-001.yaml +++ b/artifacts/verification/FV-FALCON-PREFLIGHT-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-PREFLIGHT-001 type: sw-verification title: "Pre-flight BIT + arming gate — relay-preflight tests + exhaustive Kani (falcon v1.53)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-PREFLIGHT-P01. The relay-preflight crate (no_std/ no_alloc/forbid-unsafe): PreflightChecks + arm_check. 4 unit tests diff --git a/artifacts/verification/FV-FALCON-RATE-001.yaml b/artifacts/verification/FV-FALCON-RATE-001.yaml index 122fd50..8909800 100644 --- a/artifacts/verification/FV-FALCON-RATE-001.yaml +++ b/artifacts/verification/FV-FALCON-RATE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-RATE-001 type: sw-verification title: "Unit + property + closed-loop SITL for relay-rate (v0.3)" - status: approved + status: verified description: > v0.3 verification of the body-rate PID controller (`relay-rate`) and the closed-loop pure-Rust SITL bench diff --git a/artifacts/verification/FV-FALCON-RC-001.yaml b/artifacts/verification/FV-FALCON-RC-001.yaml index afbe7d2..74b4926 100644 --- a/artifacts/verification/FV-FALCON-RC-001.yaml +++ b/artifacts/verification/FV-FALCON-RC-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-RC-001 type: sw-verification title: "Manual modes (Stabilized / Acro) — relay-rc tests + Kani clamp proofs (falcon v1.46)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-RC-P01. The relay-rc crate (no_std/no_alloc/ forbid-unsafe) maps RC sticks to Stabilized attitude / Acro rate setpoints. diff --git a/artifacts/verification/FV-FALCON-RC-002.yaml b/artifacts/verification/FV-FALCON-RC-002.yaml index 000d737..4559c9a 100644 --- a/artifacts/verification/FV-FALCON-RC-002.yaml +++ b/artifacts/verification/FV-FALCON-RC-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-RC-002 type: sw-verification title: "SBUS wire decode — relay-rc tests + Kani unpack-bounded proof (RC-P02, v1.88)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-RC-P02. The relay-rc crate (no_std/no_alloc/ forbid-unsafe) gains the SBUS verified-decode lane: a 25-byte S.BUS frame diff --git a/artifacts/verification/FV-FALCON-RC-003.yaml b/artifacts/verification/FV-FALCON-RC-003.yaml index bd32a3c..eee2281 100644 --- a/artifacts/verification/FV-FALCON-RC-003.yaml +++ b/artifacts/verification/FV-FALCON-RC-003.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-RC-003 type: sw-verification title: "CRSF wire decode — relay-rc tests + Kani unpack/CRC-bounded proof (RC-P03, v1.89)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-RC-P03. relay-rc gains the CRSF (TBS Crossfire / ExpressLRS) verified-decode lane: a 26-byte RC_CHANNELS_PACKED frame diff --git a/artifacts/verification/FV-FALCON-READINESS-001.yaml b/artifacts/verification/FV-FALCON-READINESS-001.yaml index 8b7c6ac..db13281 100644 --- a/artifacts/verification/FV-FALCON-READINESS-001.yaml +++ b/artifacts/verification/FV-FALCON-READINESS-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-READINESS-001 type: sw-verification title: "v1.0-practical readiness review + clean-room re-verification of the v1.8–v1.14 arc (v1.15.0)" - status: approved + status: verified description: > The capstone readiness review for the v1.8 -> v1.14 hardware-abstraction arc, recorded in docs/dossier/v1.0-practical-readiness.md: a diff --git a/artifacts/verification/FV-FALCON-RUNAWAY-001.yaml b/artifacts/verification/FV-FALCON-RUNAWAY-001.yaml index 10fa568..9852f71 100644 --- a/artifacts/verification/FV-FALCON-RUNAWAY-001.yaml +++ b/artifacts/verification/FV-FALCON-RUNAWAY-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-RUNAWAY-001 type: sw-verification title: "Attitude-runaway flight termination — FSM Kani + in-flight detector (falcon v1.99 expanded failsafe)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-RUNAWAY-P01: a sustained unrecoverable tilt cuts the motors via a new FSM termination state. diff --git a/artifacts/verification/FV-FALCON-SENSVOTE-001.yaml b/artifacts/verification/FV-FALCON-SENSVOTE-001.yaml index 80324cc..d70f417 100644 --- a/artifacts/verification/FV-FALCON-SENSVOTE-001.yaml +++ b/artifacts/verification/FV-FALCON-SENSVOTE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SENSVOTE-001 type: sw-verification title: "Sensor voting + GPS-loss fallback — relay-sensvote tests + Kani (falcon v1.50)" - status: approved + status: verified description: > Verifies SWREQ-FALCON-SENSVOTE-P01. The relay-sensvote crate (no_std/ no_alloc/forbid-unsafe): median3 / vote3 / median3_vec (NaN-safe, diff --git a/artifacts/verification/FV-FALCON-SHIELD-001.yaml b/artifacts/verification/FV-FALCON-SHIELD-001.yaml index 828d8e7..cb7135f 100644 --- a/artifacts/verification/FV-FALCON-SHIELD-001.yaml +++ b/artifacts/verification/FV-FALCON-SHIELD-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SHIELD-001 type: sw-verification title: "Verified simplex shield — Kani safety contract + recoverable-set predicate + containment demo (v0.28)" - status: implemented + status: verified description: > Verification of the v0.28 runtime-assurance shield: diff --git a/artifacts/verification/FV-FALCON-SIM-002.yaml b/artifacts/verification/FV-FALCON-SIM-002.yaml index b1dfe7f..429e5ac 100644 --- a/artifacts/verification/FV-FALCON-SIM-002.yaml +++ b/artifacts/verification/FV-FALCON-SIM-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIM-002 type: sw-verification title: "PX4-SITL round-trip: falcon RTL drives PX4 home via COMMAND_LONG (v0.14.2)" - status: approved + status: verified description: > v0.14.2 closes the round-trip the v0.14.0 PX4-SITL loop stopped one step short of: when the verified relay-lc diff --git a/artifacts/verification/FV-FALCON-SIM-003.yaml b/artifacts/verification/FV-FALCON-SIM-003.yaml index df68091..56c9f28 100644 --- a/artifacts/verification/FV-FALCON-SIM-003.yaml +++ b/artifacts/verification/FV-FALCON-SIM-003.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIM-003 type: sw-verification title: "Gazebo SITL scaffold — Physics trait + MockPhysics + Gazebo stub (v0.16.1)" - status: approved + status: verified description: > v0.16.1 lands the Gazebo SITL backend scaffold called for in docs/SIMULATOR.md (v0.15.0) option C. The scaffold is the diff --git a/artifacts/verification/FV-FALCON-SIM-004.yaml b/artifacts/verification/FV-FALCON-SIM-004.yaml index 78792b3..2261105 100644 --- a/artifacts/verification/FV-FALCON-SIM-004.yaml +++ b/artifacts/verification/FV-FALCON-SIM-004.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIM-004 type: sw-verification title: "Real gz-transport-rs Gazebo bridge — falcon-sitl-gz `gazebo` feature (v0.18.0)" - status: approved + status: verified description: > v0.18.0 promotes `examples/falcon-sitl-gz`'s `GazeboPhysics` from the v0.16.1 stub (returns zeros, prints warning) to a diff --git a/artifacts/verification/FV-FALCON-SIM-014.yaml b/artifacts/verification/FV-FALCON-SIM-014.yaml index 72bd678..ebcc714 100644 --- a/artifacts/verification/FV-FALCON-SIM-014.yaml +++ b/artifacts/verification/FV-FALCON-SIM-014.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIM-014 type: sw-verification title: "SIM-P02 review — simulator landscape analysis + Gazebo-bridge path (docs/SIMULATOR.md)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-SIM-P02, a documentation requirement (req-type: documentation, doc: docs/SIMULATOR.md). Verification method is review: diff --git a/artifacts/verification/FV-FALCON-SIMMC-001.yaml b/artifacts/verification/FV-FALCON-SIMMC-001.yaml index 33c6e7c..90576a3 100644 --- a/artifacts/verification/FV-FALCON-SIMMC-001.yaml +++ b/artifacts/verification/FV-FALCON-SIMMC-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIMMC-001 type: sw-verification title: "Monte-Carlo simulation campaigns — dispersed closed-loop safety verification + named CI gate (v1.109)" - status: implemented + status: verified release: falcon-v1.109.0 description: > Turns the single-condition closed-loop point-tests into large randomised diff --git a/artifacts/verification/FV-FALCON-SIMMC-003.yaml b/artifacts/verification/FV-FALCON-SIMMC-003.yaml index 07c6e5a..9012c90 100644 --- a/artifacts/verification/FV-FALCON-SIMMC-003.yaml +++ b/artifacts/verification/FV-FALCON-SIMMC-003.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIMMC-003 type: sw-verification title: "Estimator-robustness campaign — IEKF under dispersed sensor noise + GNSS dropout (v1.111)" - status: implemented + status: verified release: falcon-v1.111.0 description: > The first genuinely STOCHASTIC dispersion campaign (the attitude/failsafe diff --git a/artifacts/verification/FV-FALCON-SIMMC-004.yaml b/artifacts/verification/FV-FALCON-SIMMC-004.yaml index a3c0ce3..8a56c7c 100644 --- a/artifacts/verification/FV-FALCON-SIMMC-004.yaml +++ b/artifacts/verification/FV-FALCON-SIMMC-004.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIMMC-004 type: sw-verification title: "Maneuvering-truth estimator + GNSS-spoof-injection campaigns (v1.112 slice 1)" - status: implemented + status: verified release: falcon-v1.112.0 description: > Two stochastic estimator campaigns extending the static-hover one diff --git a/artifacts/verification/FV-FALCON-SIMMC-005.yaml b/artifacts/verification/FV-FALCON-SIMMC-005.yaml index 859a9f1..7ba9e53 100644 --- a/artifacts/verification/FV-FALCON-SIMMC-005.yaml +++ b/artifacts/verification/FV-FALCON-SIMMC-005.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIMMC-005 type: sw-verification title: "Motor-out recovery under DISPERSION — actuator noise + wind (v1.112 slice 3)" - status: implemented + status: verified release: falcon-v1.112.0 description: > Upgrades the clean-plant motor-out campaign (FV-FALCON-FAULT-002 / diff --git a/artifacts/verification/FV-FALCON-SIMMC-006.yaml b/artifacts/verification/FV-FALCON-SIMMC-006.yaml index 5c83b6d..fb74792 100644 --- a/artifacts/verification/FV-FALCON-SIMMC-006.yaml +++ b/artifacts/verification/FV-FALCON-SIMMC-006.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SIMMC-006 type: sw-verification title: "Mission / waypoint corridor-tracking campaign — real PosController under dispersion (v1.112 slice 2)" - status: implemented + status: verified release: falcon-v1.112.0 description: > A NEW behaviour in the dispersion deck: waypoint mission tracking. Drives diff --git a/artifacts/verification/FV-FALCON-SITLCORE-001.yaml b/artifacts/verification/FV-FALCON-SITLCORE-001.yaml index 8913ba1..b6102ed 100644 --- a/artifacts/verification/FV-FALCON-SITLCORE-001.yaml +++ b/artifacts/verification/FV-FALCON-SITLCORE-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SITLCORE-001 type: sw-verification title: "FlightCore-in-the-loop — the production core flies the SITL plant through the FlightBackend seam (v1.113)" - status: implemented + status: verified release: falcon-v1.113.0 description: > Closes the orphaned-core gap in the Gazebo SITL bench: every prior diff --git a/artifacts/verification/FV-FALCON-SPOOF-001.yaml b/artifacts/verification/FV-FALCON-SPOOF-001.yaml index fe2836c..bfcbbcb 100644 --- a/artifacts/verification/FV-FALCON-SPOOF-001.yaml +++ b/artifacts/verification/FV-FALCON-SPOOF-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SPOOF-001 type: sw-verification title: "Position-fix spoof/fault FDI — Kani gate+CUSUM contracts + deterministic spoof tests + real-gz hold demo (v0.37)" - status: approved + status: verified description: > Verification of the v0.37 position-fix fault/spoof robustness: diff --git a/artifacts/verification/FV-FALCON-SUPLAND-001.yaml b/artifacts/verification/FV-FALCON-SUPLAND-001.yaml index 962d071..d1b2dc1 100644 --- a/artifacts/verification/FV-FALCON-SUPLAND-001.yaml +++ b/artifacts/verification/FV-FALCON-SUPLAND-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SUPLAND-001 type: sw-verification title: "FlightSupervisor engages the velocity-landing in Land mode (v1.29.0)" - status: approved + status: verified description: > Verification of the v1.29.0 supervisor-landing integration (falcon-core tests pass — 32, clippy clean, embedded builds). v1.27 built the diff --git a/artifacts/verification/FV-FALCON-SUPV-001.yaml b/artifacts/verification/FV-FALCON-SUPV-001.yaml index 897a571..fb79e0f 100644 --- a/artifacts/verification/FV-FALCON-SUPV-001.yaml +++ b/artifacts/verification/FV-FALCON-SUPV-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-SUPV-001 type: sw-verification title: "Autonomy supervisor — geofence→RTL actuation + battery failsafe through the HAL (v1.8.0)" - status: approved + status: verified description: > Verification of the v1.8.0 FlightSupervisor (falcon-core) wiring the relay-fsm FSM into the loop with actuated failsafes (7 falcon-core tests diff --git a/artifacts/verification/FV-FALCON-TOUCHDOWN-001.yaml b/artifacts/verification/FV-FALCON-TOUCHDOWN-001.yaml index a0b4a6b..03e9cc4 100644 --- a/artifacts/verification/FV-FALCON-TOUCHDOWN-001.yaml +++ b/artifacts/verification/FV-FALCON-TOUCHDOWN-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-TOUCHDOWN-001 type: sw-verification title: "Velocity-based touchdown lands through ground effect (v1.27.0)" - status: approved + status: verified description: > Verification of the v1.27.0 velocity-based touchdown controller (31 falcon-core tests pass, clippy clean, embedded builds), the first diff --git a/artifacts/verification/FV-FALCON-TQ-001.yaml b/artifacts/verification/FV-FALCON-TQ-001.yaml index 44c9d89..bd61c8b 100644 --- a/artifacts/verification/FV-FALCON-TQ-001.yaml +++ b/artifacts/verification/FV-FALCON-TQ-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-TQ-001 type: sw-verification title: "Tool-qualification records for Verus / Kani / miri / witness / spar (v0.14.3)" - status: approved + status: verified description: > v0.14.3 lands the cross-cutting tool-qualification dossier under `docs/dossier/tool-qualification/`. Five TQ records, diff --git a/artifacts/verification/FV-FALCON-TRAJ-001.yaml b/artifacts/verification/FV-FALCON-TRAJ-001.yaml index cfd8d45..2239107 100644 --- a/artifacts/verification/FV-FALCON-TRAJ-001.yaml +++ b/artifacts/verification/FV-FALCON-TRAJ-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-TRAJ-001 type: sw-verification title: "Trajectory generation — Mueller quintic + sound jerk bound + flatness feedforward + waypoint mission (v0.27)" - status: implemented + status: verified description: > Verification of the v0.27 trajectory stack: diff --git a/artifacts/verification/FV-FALCON-TRAJ-002.yaml b/artifacts/verification/FV-FALCON-TRAJ-002.yaml index 32fcef5..f054613 100644 --- a/artifacts/verification/FV-FALCON-TRAJ-002.yaml +++ b/artifacts/verification/FV-FALCON-TRAJ-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-TRAJ-002 type: sw-verification title: "Reference governor — Kani gate bound + monotone-advance tests + flight falsification (v0.36)" - status: approved + status: verified description: > Verification of the v0.36 reference governor (relay-traj RefGovernor): diff --git a/artifacts/verification/FV-FALCON-TURB-001.yaml b/artifacts/verification/FV-FALCON-TURB-001.yaml index b9d9ec5..101d220 100644 --- a/artifacts/verification/FV-FALCON-TURB-001.yaml +++ b/artifacts/verification/FV-FALCON-TURB-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-TURB-001 type: sw-verification title: "Bounded position hold under Dryden-like turbulence (v1.25.0)" - status: approved + status: verified description: > Verification of the v1.25.0 turbulence layer (30 falcon-core tests pass, clippy clean, embedded builds), the final realism arc release (10 of 10): diff --git a/artifacts/verification/FV-FALCON-UAM-001.yaml b/artifacts/verification/FV-FALCON-UAM-001.yaml index bedce6d..07a27c1 100644 --- a/artifacts/verification/FV-FALCON-UAM-001.yaml +++ b/artifacts/verification/FV-FALCON-UAM-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-UAM-001 type: sw-verification title: "Untethered multi-waypoint mission — relay-sc RTS dispatch in SITL (v0.9)" - status: approved + status: verified description: > v0.9 verification of the untethered autonomous-mission path: the falcon-sitl-hover `untethered` scenario. diff --git a/artifacts/verification/FV-FALCON-WIND-001.yaml b/artifacts/verification/FV-FALCON-WIND-001.yaml index 49bd1a5..d9b1e0c 100644 --- a/artifacts/verification/FV-FALCON-WIND-001.yaml +++ b/artifacts/verification/FV-FALCON-WIND-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-WIND-001 type: sw-verification title: "Wind rejection via position-loop integral (v1.16.0)" - status: approved + status: verified description: > Verification of the v1.16.0 wind layer (15 falcon-core tests pass, clippy clean, embedded builds), the first SITL-realism release: diff --git a/artifacts/verification/FV-FALCON-WINDFS-001.yaml b/artifacts/verification/FV-FALCON-WINDFS-001.yaml index fc73723..49ff267 100644 --- a/artifacts/verification/FV-FALCON-WINDFS-001.yaml +++ b/artifacts/verification/FV-FALCON-WINDFS-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-WINDFS-001 type: sw-verification title: "High-wind failsafe — saturation+tilt → RTL, distinct from termination (falcon v1.101)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-WINDFS-P01: sustained control saturation while leaning hard (but short of a tumble) commands an RTL-class recovery. diff --git a/artifacts/verification/FV-FALCON-WORLD-001.yaml b/artifacts/verification/FV-FALCON-WORLD-001.yaml index 70081da..8b5c8dd 100644 --- a/artifacts/verification/FV-FALCON-WORLD-001.yaml +++ b/artifacts/verification/FV-FALCON-WORLD-001.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-WORLD-001 type: sw-verification title: "v0.1 end-to-end UDP heartbeat exchange test" - status: approved + status: verified description: > Integration test in examples/falcon-hello demonstrating the v0.1 acceptance criterion: vehicle and GCS exchange MAVLink diff --git a/artifacts/verification/FV-FALCON-WORLD-002.yaml b/artifacts/verification/FV-FALCON-WORLD-002.yaml index 202fee4..53824c1 100644 --- a/artifacts/verification/FV-FALCON-WORLD-002.yaml +++ b/artifacts/verification/FV-FALCON-WORLD-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-FALCON-WORLD-002 type: sw-verification title: "WORLD-P02: variant worlds share one mixer-agnostic control cascade (v1.87)" - status: implemented + status: verified description: > Verifies SWREQ-FALCON-WORLD-P02 (all falcon-* worlds reuse the same relay-ekf/rate/att/pos cascade unmodified; only the relay-mix-* mixer and diff --git a/artifacts/verification/FV-RELAY-KANICI-002.yaml b/artifacts/verification/FV-RELAY-KANICI-002.yaml index 0d8160d..07d8f5f 100644 --- a/artifacts/verification/FV-RELAY-KANICI-002.yaml +++ b/artifacts/verification/FV-RELAY-KANICI-002.yaml @@ -2,7 +2,7 @@ artifacts: - id: FV-RELAY-KANICI-002 type: sw-verification title: "Flight-critical control + estimator Kani harnesses enforced in CI (orphaned-proof closure)" - status: implemented + status: verified release: falcon-v1.104.0 description: > Closes the highest-value subset of a systemic orphaned-proof gap. A