From 295652a089c36ddda547ba058718c1d63a56dc91 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 26 Aug 2026 06:36:19 +0200 Subject: [PATCH] verify(trace): promote 105 verification artifacts from EXECUTED gate evidence (TRACE-P02) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The right side of the V was almost entirely unpromoted: 22 of 247 requirements `verified`, with the evidence already existing and simply unbound. This binds the part that a gate run can actually justify. METHOD — executed evidence, not a `verifies` link. A full sweep (`--filter '(has-tag "falcon")'`) ran 323 steps with 0 FAIL. An artifact qualifies only if it had >=1 step that genuinely EXECUTED and none that failed. Skipped steps do not count: bench-only, `enforced-by-kani-gate` and `skip-no-steps` are all exclusions, because "the gate did not run it" is not evidence that it passes. artifacts in the sweep 162 >=1 EXECUTED step, zero failures 130 <- promoted only skipped steps 32 <- left unpromoted, deliberately any FAIL 0 Net: 105 promoted here (the other 25 were already `verified`). Verification artifacts: 130 verified / 123 approved / 34 implemented. --- A THIRD CATEGORY TRACE-P02 DID NOT ANTICIPATE, FOUND BY DOING IT --- The mechanical sweep initially promoted SIX artifacts whose own text says they must NOT be verified: FV-FALCON-OCI-002 "stays `implemented` until the fuse is run" FV-FALCON-OCI-003 wasm.directory criteria (b) and (c) NOT MET FV-FALCON-OCI-004 kill-criterion owned by gale/meld, unrun FV-FALCON-OCI-005 ditto FV-FALCON-PERF-002 criterion (d), the PX4 head-to-head, not done (#362) FV-FALCON-REL-001 failure injection not run All six have PASSING executed steps. The gate result is real. It is also NOT SUFFICIENT, because each names a criterion the gate cannot check — an external kill-criterion, a live-page fetch, a comparison nobody has run. TRACE-P02 anticipated two populations: gate-runnable (promote) and bench-only (waive). This is a third: **gate-passing AND self-blocked**. Promoting them would have asserted precisely the outcomes those criteria exist to test — the error v1.133 avoided and that jess's meld run then vindicated by REJECTING. All six reverted to `implemented`. The rule this establishes: an artifact that names an undischarged criterion is excluded from mechanical promotion no matter how green its steps are. Gate evidence is necessary, never sufficient. WHAT IS DELIBERATELY NOT PROMOTED: - 32 artifacts whose steps only skipped (bench-only / kani-enforced) - the 6 self-blocked above - 45 artifacts with NO steps at all — separately tracked; they cannot be evidence as they stand and need steps written or an honest demotion - requirements themselves — this promotes VERIFIERS; requirement promotion follows once their verifiers are all `verified` Code-free, per the two-commit rule. rivet validate: PASS, exit 0. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/verification/FV-FALCON-ADRC-002.yaml | 2 +- artifacts/verification/FV-FALCON-ATMOS-001.yaml | 2 +- artifacts/verification/FV-FALCON-ATT-001.yaml | 2 +- artifacts/verification/FV-FALCON-AVOID-001.yaml | 2 +- artifacts/verification/FV-FALCON-BARO-001.yaml | 2 +- artifacts/verification/FV-FALCON-BAROMAGDRV-001.yaml | 2 +- artifacts/verification/FV-FALCON-BATTERY-001.yaml | 2 +- artifacts/verification/FV-FALCON-CALIB-001.yaml | 2 +- artifacts/verification/FV-FALCON-CMDLONG-001.yaml | 2 +- artifacts/verification/FV-FALCON-COV-004.yaml | 2 +- artifacts/verification/FV-FALCON-COV-005.yaml | 2 +- artifacts/verification/FV-FALCON-CPREV-001.yaml | 2 +- artifacts/verification/FV-FALCON-DC-001.yaml | 2 +- artifacts/verification/FV-FALCON-DC-002.yaml | 2 +- artifacts/verification/FV-FALCON-DC-003.yaml | 2 +- artifacts/verification/FV-FALCON-DC-004.yaml | 2 +- artifacts/verification/FV-FALCON-DC-CONFORMANCE.yaml | 2 +- artifacts/verification/FV-FALCON-DRAG-001.yaml | 2 +- artifacts/verification/FV-FALCON-EKF-001.yaml | 2 +- artifacts/verification/FV-FALCON-EKF-002.yaml | 2 +- artifacts/verification/FV-FALCON-EKF-STUB-001.yaml | 2 +- artifacts/verification/FV-FALCON-ESCDRV-001.yaml | 2 +- artifacts/verification/FV-FALCON-FAULT-001.yaml | 2 +- artifacts/verification/FV-FALCON-FAULT-002.yaml | 2 +- artifacts/verification/FV-FALCON-FAULT-003.yaml | 2 +- artifacts/verification/FV-FALCON-FLOWRANGE-001.yaml | 2 +- artifacts/verification/FV-FALCON-FSAFE-001.yaml | 2 +- artifacts/verification/FV-FALCON-FSM-001.yaml | 2 +- artifacts/verification/FV-FALCON-GEO-001.yaml | 2 +- artifacts/verification/FV-FALCON-GEO-002.yaml | 2 +- artifacts/verification/FV-FALCON-GNDEFFECT-001.yaml | 2 +- artifacts/verification/FV-FALCON-GNSS-001.yaml | 2 +- artifacts/verification/FV-FALCON-GNSSDRV-001.yaml | 2 +- artifacts/verification/FV-FALCON-GZGE-001.yaml | 2 +- artifacts/verification/FV-FALCON-HAL-001.yaml | 2 +- artifacts/verification/FV-FALCON-HAL-002.yaml | 2 +- artifacts/verification/FV-FALCON-HAL-003.yaml | 2 +- artifacts/verification/FV-FALCON-HITL-001.yaml | 2 +- artifacts/verification/FV-FALCON-HITL-002.yaml | 2 +- artifacts/verification/FV-FALCON-HWSEAM-001.yaml | 2 +- artifacts/verification/FV-FALCON-IEKF-001.yaml | 2 +- artifacts/verification/FV-FALCON-IMUBIAS-001.yaml | 2 +- artifacts/verification/FV-FALCON-IMUDRV-001.yaml | 2 +- artifacts/verification/FV-FALCON-LINK-001.yaml | 2 +- artifacts/verification/FV-FALCON-LOG-001.yaml | 2 +- artifacts/verification/FV-FALCON-LYAP-001.yaml | 2 +- artifacts/verification/FV-FALCON-MATHSEAM-001.yaml | 2 +- artifacts/verification/FV-FALCON-MATHSEAM-002.yaml | 2 +- artifacts/verification/FV-FALCON-MAVBRIDGE-001.yaml | 2 +- artifacts/verification/FV-FALCON-MAVLINK-001.yaml | 2 +- artifacts/verification/FV-FALCON-MISSION-001.yaml | 2 +- artifacts/verification/FV-FALCON-MISSIONDL-001.yaml | 2 +- artifacts/verification/FV-FALCON-MISSIONUP-001.yaml | 2 +- artifacts/verification/FV-FALCON-MIX-001.yaml | 2 +- artifacts/verification/FV-FALCON-MIX-003.yaml | 2 +- artifacts/verification/FV-FALCON-MIX-004.yaml | 2 +- artifacts/verification/FV-FALCON-MIXMULTI-001.yaml | 2 +- artifacts/verification/FV-FALCON-MODE-001.yaml | 2 +- artifacts/verification/FV-FALCON-MODEXTRA-001.yaml | 2 +- artifacts/verification/FV-FALCON-MOTORDYN-001.yaml | 2 +- artifacts/verification/FV-FALCON-NID-001.yaml | 2 +- artifacts/verification/FV-FALCON-NID-002.yaml | 2 +- artifacts/verification/FV-FALCON-OFFB-001.yaml | 2 +- artifacts/verification/FV-FALCON-PACE-001.yaml | 2 +- artifacts/verification/FV-FALCON-PARAM-001.yaml | 2 +- artifacts/verification/FV-FALCON-PARAM-002.yaml | 2 +- artifacts/verification/FV-FALCON-PATH-001.yaml | 2 +- artifacts/verification/FV-FALCON-PERF-001.yaml | 2 +- artifacts/verification/FV-FALCON-PIPELINE-001.yaml | 2 +- artifacts/verification/FV-FALCON-POS-001.yaml | 2 +- artifacts/verification/FV-FALCON-PREARM-001.yaml | 2 +- artifacts/verification/FV-FALCON-PREARM-002.yaml | 2 +- artifacts/verification/FV-FALCON-PREFLIGHT-001.yaml | 2 +- artifacts/verification/FV-FALCON-RATE-001.yaml | 2 +- artifacts/verification/FV-FALCON-RC-001.yaml | 2 +- artifacts/verification/FV-FALCON-RC-002.yaml | 2 +- artifacts/verification/FV-FALCON-RC-003.yaml | 2 +- artifacts/verification/FV-FALCON-READINESS-001.yaml | 2 +- artifacts/verification/FV-FALCON-RUNAWAY-001.yaml | 2 +- artifacts/verification/FV-FALCON-SENSVOTE-001.yaml | 2 +- artifacts/verification/FV-FALCON-SHIELD-001.yaml | 2 +- artifacts/verification/FV-FALCON-SIM-002.yaml | 2 +- artifacts/verification/FV-FALCON-SIM-003.yaml | 2 +- artifacts/verification/FV-FALCON-SIM-004.yaml | 2 +- artifacts/verification/FV-FALCON-SIM-014.yaml | 2 +- artifacts/verification/FV-FALCON-SIMMC-001.yaml | 2 +- artifacts/verification/FV-FALCON-SIMMC-003.yaml | 2 +- artifacts/verification/FV-FALCON-SIMMC-004.yaml | 2 +- artifacts/verification/FV-FALCON-SIMMC-005.yaml | 2 +- artifacts/verification/FV-FALCON-SIMMC-006.yaml | 2 +- artifacts/verification/FV-FALCON-SITLCORE-001.yaml | 2 +- artifacts/verification/FV-FALCON-SPOOF-001.yaml | 2 +- artifacts/verification/FV-FALCON-SUPLAND-001.yaml | 2 +- artifacts/verification/FV-FALCON-SUPV-001.yaml | 2 +- artifacts/verification/FV-FALCON-TOUCHDOWN-001.yaml | 2 +- artifacts/verification/FV-FALCON-TQ-001.yaml | 2 +- artifacts/verification/FV-FALCON-TRAJ-001.yaml | 2 +- artifacts/verification/FV-FALCON-TRAJ-002.yaml | 2 +- artifacts/verification/FV-FALCON-TURB-001.yaml | 2 +- artifacts/verification/FV-FALCON-UAM-001.yaml | 2 +- artifacts/verification/FV-FALCON-WIND-001.yaml | 2 +- artifacts/verification/FV-FALCON-WINDFS-001.yaml | 2 +- artifacts/verification/FV-FALCON-WORLD-001.yaml | 2 +- artifacts/verification/FV-FALCON-WORLD-002.yaml | 2 +- artifacts/verification/FV-RELAY-KANICI-002.yaml | 2 +- 105 files changed, 105 insertions(+), 105 deletions(-) diff --git a/artifacts/verification/FV-FALCON-ADRC-002.yaml b/artifacts/verification/FV-FALCON-ADRC-002.yaml index 0bbc2688..2a16ece9 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 fdba405a..9c1e3813 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 2f92f1df..10bebdb5 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 eeef5b68..01fe3bef 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 24ca0d58..033c0182 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 af78e663..240dbac3 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 4f66e31b..8de89b4e 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 2587810d..7ed8e5fe 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 15ea81bf..e0030aa1 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 c7b705c6..3757fe8f 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 17193bcc..5adfde79 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 43b6b47b..8d4bf462 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 39cf71ec..719de971 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 71edd45d..10095cdd 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 8a234c0d..60552ac8 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 447b309f..0aec0364 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 9e47460b..38e58eae 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 e0bb2ac5..05791bc8 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 a5c9c813..6c786a09 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 9571338c..4bf920dd 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 c70393b7..03c5fc89 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 90b667e7..c0a95b17 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 cce016a6..a572b943 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 7a4644ef..4dbb71b2 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 09a953ab..6880bfda 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 f6e0432c..a7af63d7 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 3f561c2a..02846f51 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 d6e3da2f..e7446349 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 d0677ef9..d8db12d7 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 3c48f94f..52110f1a 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 ebae7ffb..abd07926 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 aac8e969..36330ac3 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 562df240..c7936175 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 1bedde1c..3817732e 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 cbfd1e0c..b2b1170b 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 e913fc82..a6c5590f 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 5b5b5e21..d5f70f81 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 897f5833..618b5d7c 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 6166f9ff..2a715700 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 f825d341..669bbfaa 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 8c79764b..1e36fb2c 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 f587b9af..c2aca5a4 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 79e0943e..5093b42a 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 9bfb6c14..279341c1 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 03a798c4..71ceca48 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 e9688ac8..71154039 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 5428cea0..ba09ddb5 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 8987aeaf..cb743b53 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 399967b6..cb84bcea 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 b16cd21c..f67b6540 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 0d9f05d8..fee2074b 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 379191d5..187b2525 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 9cca1d30..49bd8032 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 05cdc30c..1d6eae88 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 240b413b..69294c0a 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 134a0041..0ff42d36 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 e8b6dbc0..63cd1611 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 5a3a8809..d110999e 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 104de74f..71df557b 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 6dd7cd11..87b93e49 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 bb55a208..a97317d1 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 d91ba858..c0657bc3 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 f48b4508..3b339ce7 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 e1a12b41..3e18ac32 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 5fd48de3..b7beaab1 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 d63b49b9..fb1fe042 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 ecd21061..b7ca5a25 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 99c1af2f..646bb41c 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 7cb9953e..97b19adc 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 6af41c3d..369a025f 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 7dd40308..a2eb160f 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 46905b1e..10bed269 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 aacdf8ed..42a14c46 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 122fd501..8909800a 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 afbe7d24..74b4926d 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 000d7379..4559c9a9 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 bd32a3c3..eee2281d 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 8b7c6ac6..db132816 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 10fa5689..9852f71d 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 80324cc3..d70f417c 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 828d8e72..cb7135f0 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 b1dfe7f2..429e5ac9 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 df68091e..56c9f289 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 78792b39..22611059 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 72bd678f..ebcc7140 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 33c6e7c3..90576a33 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 07c6e5a7..9012c907 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 a3c0ce30..8a56c7ce 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 859a9f1a..7ba9e53f 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 5c83b6da..fb747923 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 8913ba1d..b6102ed6 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 fe2836cd..bfcbbcbd 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 962d071b..d1b2dc16 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 897a5716..fb79e0f1 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 a0b4a6b0..03e9cc41 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 44c9d893..bd61c8b9 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 cfd8d45c..22391075 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 32fcef5e..f054613b 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 b9d9ec56..101d220d 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 bedce6d2..07a27c15 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 49bd1a50..d9b1e0c6 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 fc737232..49ff2676 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 70081da8..8b5c8ddb 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 202fee49..53824c19 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 0d8160df..07d8f5f7 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