feat(falcon): v0.19.9 — verified arming sequencer (ARM-P01) + tip-over localization#54
Conversation
…r localization
Ships relay-arm, a Kani-verified startup state machine
(Disarmed → SpinUp → LevelHold → Armed) that gates attitude-torque
authority: the rate loop's torque reaches the mixer ONLY in Armed, and
Armed is reachable ONLY through a confirmed-level window. Replaces the
bench's ad-hoc time-only `t < 0.5 s` spawn-hold with verified time+level
gating — the "deterministic startup sequencing" called for as fix (1) in
the v0.19.7 bistability diagnosis.
Verification — Kani, not Verus (the tilt compare is f32; like
relay-mix-quad this is off the integer Verus track). The gating invariant
is INDUCTIVE over one tick(), so the bounded check covers all
input sequences:
cargo kani verify_arming_torque_gated → 143 checks SUCCESSFUL
(torque_authority ⟺ Armed; a new entry into Armed comes only from
LevelHold with the level gate satisfied; phase ∈ [0,3];
thrust_scale ∈ [0,1] finite)
cargo kani verify_arming_total → 137 checks SUCCESSFUL
(panic-free + thrust bounded for NaN/∞ tilt, zero spin-up)
Plus proptest + 5 unit tests.
FALSIFICATION (the empirical value): I set out to "kill RC#1 startup
tip-over" — the gz data falsified that framing. With the correct NavSat
home, the gated AND ungated startups both hand off a LEVEL body (0°
through arming at 0.40 s); the body then holds level ~3.5 s and only tips
(~88°) once the position loop dominates. The tip-over is a DOWNSTREAM
residual (relay-pos thrust normalisation + RC#3 EKF-attitude-during-accel),
NOT a spawn transient. The arming sequencer is verified, correct, and a
prerequisite building block — but it is NOT what unblocks position-hold.
Publishing this localizes the v0.19.10+ target precisely.
Regression gate: gz alt-rate reliable hover is unaffected — 3/3
consecutive PASS at ~0.20 m, identical to v0.19.8's 4/4.
Ships:
- crates/relay-arm: ArmingSequencer + ArmingConfig + Kani harnesses +
tests (new workspace member).
- examples/falcon-sitl-gz: sequencer wired into alt-rate AND the full
closed-loop cascade (which also adopts mix_thrust_floor); body_tilt_rad
helper; `arming` / `arming-ungated` diagnostic scenarios.
- SWREQ-FALCON-ARM-P01 + FV-FALCON-ARM-001 + rollout v0.19.9 entry.
- bench-evidence/gz-sim/2026-05-29-v0.19.9-*.md (incl. the -488 m
NavSat-home methodology trap).
Honestly NOT claimed: that arming makes full position-hold hover (it does
not — run_peak ~88°), nor that a gz "arming-check PASS" means the quad
hovers (PASS is scoped to the startup handoff). Full position-hold remains
the residual, now localized to relay-pos thrust + RC#3 for v0.19.10+.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.12s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s --- scenario: mission --- running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 20 tests test result: ok. 20 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 20 tests test result: ok. 20 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.28s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.04s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.65s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s --- scenario: step --- running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s falcon-hitl-rfspoof: backend=stub duration=5s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.11s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s --- scenario: attitude --- running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s [falcon-hello-demo] building release binary... running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.85s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 5 tests test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s --- noise=0 (deterministic) --- running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 1 test test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 16 filtered out; finished in 0.02s running 14 tests test result: ok. 14 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.05s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.08s running 14 tests test result: ok. 14 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 14 tests test result: ok. 14 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 14 tests test result: ok. 14 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.15s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.09s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s falcon verification gate (type: sw-verification, filter: (has-tag "falcon"))42 artifact(s) matched: FV-FALCON-SIM-007, FV-FALCON-ARM-001, FV-FALCON-POS-001, FV-FALCON-SIM-001, FV-FALCON-SIM-006, FV-FALCON-MAVLINK-002, FV-FALCON-NID-001, FV-FALCON-RATE-001, FV-FALCON-TQ-001, FV-FALCON-HITL-001, FV-FALCON-SIM-012, FV-FALCON-ARCH-002, FV-FALCON-SIM-002, FV-FALCON-SIM-004, FV-FALCON-ATT-001, FV-FALCON-WORLD-001, FV-FALCON-SIM-013, FV-FALCON-EKF-001, FV-FALCON-COV-005, FV-FALCON-GEO-001, FV-FALCON-PIPELINE-001, FV-FALCON-SIM-005, FV-FALCON-MIX-002, FV-FALCON-SIM-009, FV-FALCON-SIM-008, FV-FALCON-MIX-001, FV-FALCON-EKF-STUB-001, FV-FALCON-COV-003, FV-FALCON-HITL-002, FV-FALCON-ARCH-001, FV-FALCON-GEO-003, FV-FALCON-UAM-001, FV-FALCON-COV-004, FV-FALCON-MAVLINK-001, FV-FALCON-NID-002, FV-FALCON-SIM-010, FV-FALCON-COV-001, FV-FALCON-SIM-011, FV-FALCON-GEO-002, FV-FALCON-COV-002, FV-FALCON-SIM-003, FV-FALCON-FAULT-001[ skip-no-steps] FV-FALCON-SIM-007: (no steps defined) test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 16 filtered out; finished in 0.05s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.43s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 20 tests test result: ok. 20 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s Filename Regions Missed Regions Cover Functions Missed Functions Executed Lines Missed Lines Cover Branches Missed Branches Covercoverage_subjects/geofence_subject_rs/src/lib.rs 48 48 0.00% 5 5 0.00% 23 23 0.00% 0 0 -
|
| count | |
|---|---|
| Passed | 35 |
| Failed | -10 |
| Skipped (bench-only — needs hardware / sim) | 7 |
| Skipped (no steps) | 10 |
Failed artifacts
Bench-only artifacts (not run by CI)
FV-FALCON-SIM-001— PX4-SITL end-to-end loop — recipe + preset + smoke (v0.14.0)FV-FALCON-ARCH-002— spar codegen --format wit recheck — works at v0.10.0 (v0.15.0)FV-FALCON-SIM-005— gz-transport NavSat + Home projection — position-dependent loops (v0.18.1)FV-FALCON-COV-003— witness MC/DC on real Rust source — Geofence subject (v0.14.1)FV-FALCON-ARCH-001— spar AADL architectural model — falcon cascade (v0.13)FV-FALCON-GEO-003— Geofence safety path — miri UB/overflow check (v0.12, AI substitute)FV-FALCON-COV-001— witness MC/DC structural coverage — falcon pipeline wired (v0.13)
Source of truth: artifacts/verification/FV-FALCON-*.yaml.
1 participant
Summary
Ships
relay-arm, a Kani-verified startup state machine that gates attitude-torque authority —Disarmed → SpinUp → LevelHold → Armed. The rate loop's torque reaches the mixer only inArmed, andArmedis reachable only through a confirmed-level window. Replaces the bench's ad-hoc time-onlyt < 0.5 sspawn-hold with verified time+level gating (the "deterministic startup sequencing" called for as fix (1) in the v0.19.7 bistability diagnosis).Verification — Kani (inductive per tick)
The torque-gating invariant is inductive over one
tick(), so a bounded check covers all input sequences:verify_arming_torque_gatedverify_arming_totalverify_arming_torque_gatedprovestorque_authority ⟺ phase==Armed, that a new entry intoArmedcomes only fromLevelHoldwith the level gate satisfied (torque can never engage before confirmed level),phase ∈ [0,3],thrust_scale ∈ [0,1]finite. Plus proptest + 5 unit tests. Kani, not Verus: the tilt compare is f32 (same posture asrelay-mix-quad).Falsification finding (the empirical value)
I set out to "kill RC#1 startup tip-over" — the gz data falsified that framing. With the correct NavSat home, the gated and ungated startups both hand off a level body (0° through arming at 0.40 s); the body holds level ~3.5 s and only tips (~88°) once the position loop dominates. So the tip-over is a downstream residual —
relay-posthrust normalisation + RC#3 (EKF attitude during accel) — not a spawn transient. The arming sequencer is verified, correct, and a prerequisite building block, but it is not what unblocks position-hold. Publishing this localizes the v0.19.10+ target.Regression gate
gz alt-rate reliable hover unaffected: 3/3 consecutive PASS at ~0.20 m, rms ~0.21 m / 30 s — identical to v0.19.8's 4/4.
What's NOT claimed
run_peak~88°).[PASS ✓ (handoff)]+ a NOTE reporting the whole-run tip).Traceability:
SWREQ-FALCON-ARM-P01→FV-FALCON-ARM-001.rivet validatePASS.🤖 Generated with Claude Code