falcon-v1.139.0

Release falcon-v1.139.0

Verification tracks at 97ee07e1d3a1

Generated from the observed CI conclusions on the released commit by scripts/verification-tracks.rs (SWREQ-RELAY-VGATE-P04) — not written by hand.

1 track(s) DARK and 0 per-commit track(s) not run or unfinished on this commit. A dark track verified nothing for this release; treat its claims accordingly.

track	workflow	on this commit
Tests ×3, Clippy, Format	ci.yml	✅ passed
Kani bounded model checking	kani.yml	✅ passed
Verus SMT proofs	verus.yml	🔴 DARK — failure
Lean proofs	lean.yml	✅ passed
Rocq / Gappa proofs	rocq.yml	✅ passed
Gazebo SITL (native + wasm)	gazebo.yml	✅ passed
Bazel build	bazel.yml	✅ passed
Coverage	coverage.yml	✅ passed
spar AADL analysis + WIT drift	spar.yml	✅ passed
rivet verification gate	verification-gate.yml	⚪ runs on pull requests only — no run on this commit
Nightly endurance soak	soak.yml	✅ passed

Known structural gaps

A green track can still check less than it appears to. Open at release time:

• #405 — Verus cannot find core/std — every verus_test fails before verifying anything
• #418 — verus.yml's PR trigger is path-filtered on Lean paths, so Verus does not run on the PRs that change Verus code
• #410 — the required verification gate has no main backstop; its scope filter can exclude what a PR changed
• #407 — //:falcon-cascade-coverage fails to fuse; cascade MC/DC coverage has never been produced in CI
• #417 — the required gates can pass vacuously for a PR that touches only the shipped wasm components
• #436 — scheduled monitors run every few hours, not on their cron cadence
• #452 — SimBackend's accelerometer reports gravity only, so 18 closed-loop hold and estimator tests never see the vehicle accelerate