falcon-v1.140.0

falcon-v1.140.0 — "Hold"

The hold release. A position hold that stays bounded for an hour on both execution paths, judged horizontally rather than on altitude alone; the cascade transport seam published; and the root cause of the attitude ring found where no proof was looking.

What this tag actually verifies

Nine artifacts reach verified at falcon-v1.140.0, and they are the only claims this tag carries as verified:

requirement	what it asserts
SWREQ-FALCON-HOLD-P01	a stationary position hold stays bounded for 60 s on the reference gz plant
SWREQ-FALCON-ENDURANCE-P01	a position hold stays bounded for hours, on both the native and wasm paths
SWREQ-FALCON-BATTERY-P03	a pack that stops reporting in flight raises the failsafe — but only if it ever reported one
SWREQ-RELAY-MIXPROOF-P01	the MIX-P06 priority-mix bound proof holds compositionally and can fail
FLEET-P01 (via FV-RELAY-FLEET-002)	fleet starvation is measured from jobs, and hosted contention is not reported as a dead fleet

Everything else below ships as code on main and is not verified by this release. Where that matters, it is said inline.

What this release is actually about

The hold holds, and it is measured on the axis that matters. The nightly endurance soak previously ran only the native path and barred only altitude — so a run that held height while drifting away passed. Clause 3 of ENDURANCE-P01 names two axes. The soak now runs the wasm component too (#524), judges both paths horizontally (#525), and its floor was ratcheted from 120 s to the full 3600 s only after the hour had actually run four nights running (#523). Both paths now hold the hour. On the most recent scheduled run (2026-10-08, run 37764076289, the cadence that matters rather than a dispatch), the legs report final horizontal error of 0.008–0.035 m with peak excursion 0.016–0.071 m, against bars of 1.0 m and 2.0 m — roughly thirty times the margin the bars demand. Provenance, since a cited figure should name its commit: that run executed on 8bec5fc, and cdf3b74 (#539) has since touched soak.yml — but #539 changed only the cross-job notice wording, no bar or threshold, so the figures measure the same bars this tag ships.

A real filter-rate defect fixed — but not the ring. The filters were designed for 1 kHz and stepped at 250 Hz (#488), a resampling error rather than a tuning problem. The attitude ring itself is still open. #270 and #398 are both open, and SWREQ-FALCON-RATE-P05 / FV-FALCON-RATE-002 are implemented and scoped v1.142 — their fix is not on main, which is why #495 retracted an earlier "fixed" claim and #529/#538 demoted and re-scoped them. Treat the ring as an open investigation whose primary cause is understood (ESO windup under mixer saturation, measured in bench-evidence/gz-sim/) but whose fix has not landed.

Separately, v1.140's stale-aiding fallback was actively harmful and was removed: a multirotor accelerometer reads specific force along the thrust axis, so it is never a tilt reference in flight (#487, #483).

The cascade transport seam ships as code — and is NOT verified by this release. TRANSPORT-P01 lands the framing, handshake and tick contract (#504), the cascade returns state through an observer export with a seqlock (#493), and the reference host speaks the published binding with the legacy 16/54-byte frames retired (#530). ⚠️ For jess in particular, who specified this seam: SWREQ-FALCON-TRANSPORT-P01 and FV-FALCON-TRANSPORT-001/002/003 are all implemented, scoped falcon-v1.141.0. The code is in this tag and can be built against; the seam's verification is not. Do not read this release as delivering a verified transport contract.

The supervisor can say why — it reports the reason it failsafed, not only what it did (#515). Also code-only: SWREQ-FALCON-SUPERVISOR-P01 is proposed at v1.141 and blocked on jess#167, the seam reshape, so this capability is shipped but unverified.

Verification integrity — the unglamorous half

Four gates were checking less than they appeared to, and all four are fixed in this release:

• The Verus gate was path-filtered on Lean paths, so it never ran on the PRs that changed Verus code (#531, issue #418). It now also asserts it verified something, with a floor so the assertion can fail: 281 functions, 0 errors, across 19 targets on this release's commit, read from run 37881361372 (the figure was 270 when the assertion landed in #533). That refuted #405 outright.
• The required verification gate had no main backstop: nothing ever re-ran it on the merge result, so a scope filter could exclude what a PR changed and nobody would know (#535, issue #410). The backstop is observed working, not merely configured — its first schedule-event run (2026-10-09 07:58Z, run 37902164712) swept 207 artifacts on main and passed. That distinction matters here: a cron in a file is not evidence, and this repo's scheduled workflows are throttled by Actions well past their stated cadence.
• bazel.yml enumerated its targets instead of querying them, which is #407's cause rather than its symptom (#540).
• soak.yml had been rejected by Actions since 08:56 and nothing would have told us (#507); a companion check now measures whether the nightly soak ran, and its very first run falsified the claim that it had (#522).

Plus: red checks are now classified REAL / LOST / DERIVED / SUPERSEDED instead of being read at face value (#517), a green-but-stuck PR no longer needs a human to notice it (CIFLOW-P01, #511), and the branch keeper no longer authors PR heads — which had silently gated every PR's CI behind manual approval (#512).

FLEET-002 closes the round: the fleet monitor's starvation detector is now verified by a replay harness rather than by greps over the workflow text. Inverting the comparison the detector exists to protect (-lt → -ge) leaves the four grep steps 4 pass, 0 fail — blind, while the harness fails 4 of 5 fixtures and exits 1 (#541).

⚠️ Disclosures

Stated here because a green release can still have checked less than it appears to.

This release shipped WITHOUT an independent review. FV-RELAY-REVIEW-140 — the /code-review ultra checkpoint that the approved release plan places before every tag — was explicitly de-scoped by the maintainer on 2026-10-09 and moved to v1.141. The artifact was re-scoped rather than deleted, with its range pinned to falcon-v1.139.0..falcon-v1.140.0, so this diff is still reviewed before v1.141 tags rather than falling into a blind spot between two reviews. For calibration on what that gate catches: the equivalent review on v1.139 returned nine findings, including a workflow_dispatch input interpolated into a run: block on a self-hosted runner.

29 traceability inverse links are unmeasured. rivet check bidirectional fires with 29 missing allocated-to inverses (e.g. SWARCH-FALCON-001 -(allocated-from)-> SWREQ-FALCON-ATT-P01). This oracle is not run by any CI workflow, so it has never gated a release. It was not investigated before this tag and is recorded as open.

A release-gate oracle was returning false blockers. rivet check verification-evidence reports 96 of this repo's 183 named-test steps as citing tests that do not exist. All 96 are false — it matches filters as exact test names, while cargo test <filter> is a substring match over the full test path; one citation sampled per crate across all 12 affected crates exited 0 with tests passing. Filed as pulseengine/rivet#1063. Relay is insulated because its verification gate executes fields.steps[].run rather than name-matching them — but note that a bare rivet check prints help and exits 0, so wiring it in as a gate would pass vacuously.

A clean-room review of this release exists, returned DO NOT TAG, and four of its five blocking findings are fixed — the fifth is not. An independent cold-context review ran against v1.140 on 2026-10-01 (agent a02291cfdd4bf4e2b) and recommended against tagging. Its findings are reconciled here because a review whose verdict is not dispositioned in public is the same as no review:

finding	disposition
ENDURANCE-P01 — the 1 h gz hold had never run (GZ_MAX_S empty → 120 s), no wasm step existed, and GZ_FLOOR_S: 25 let a 4.8× regression pass	fixed — #523 ratcheted the floor to 3600 s, #524 added the wasm path, #525 judges both paths horizontally
BATTERY-P03 — its own falsification was met by a passing cited test; the text predated the #475/#476 correction	fixed — the text now reads "but only if it has ever had a pack", matching batt_seen && batt_missing_s > BATT_SILENCE_S
FLEET-002 — could not fail; inverting the comparison left all four grep steps green, and no replay harness was committed	fixed — #541 landed the harness, #542 promoted it on the inversion measurement
MIXPROOF-001 — steps exited 1 as written (missing working-directory) and the artifact was outside the gate's (has-tag "falcon") filter	fixed — steps now cd crates/relay-mix-quad && and the falcon tag is present
FV-FALCON-HOLD-001 — the verdict allows 2× HOLD-P01's bounds	⚠️ OPEN — #546

The open one, stated precisely: HOLD-P01 requires the vehicle "remain within 0.5 m vertically and 1.0 m horizontally … for at least 60 s" — a bound at every instant. The verdict (examples/falcon-sitl-gz/src/main.rs:2013) checks the final sample at the requirement's bound, then sets every aggregate that could see a mid-run excursion at twice it: rms_steady < 1.0 against a 0.5 m vertical bound, peak_horiz < 2.0 against a 1.0 m horizontal one. A hold that excursions to 1.9 m at t=30 s and settles by t=60 s violates the requirement and passes its own verified verification.

Nothing in this release is false on that account. The measured margin is 14–60×: the scheduled soak reports peak excursions of 0.016–0.071 m against a 1.0 m bound. The defect is that the gate would not catch a regression until it was twice as bad as the requirement allows — the VGATE family's own pattern, a green gate can check less than it claims, applied to the flagship hold requirement.

It was not fixed before this tag deliberately. Tightening a required gate's bar deserves its own PR with its own mutation evidence — proving the tightened bar can still fail, and that both legs pass it on three runs rather than one — and the tag was authorized on specific content. Disclosing the gap beat silently expanding the release. Scoped v1.141 as #546.

Two further non-blocking observations from the same review are recorded for completeness: BATT_SILENCE_S can be set to 0.0 with all 66 falcon-core tests still green, so the clause "a single dropped sample cannot trigger the failsafe either" has no test pinning it from below; and 279b0c5 (#487) changed the estimator by +224 lines and edited FV-FALCON-HOLD-001 in the same PR while leaving it verified — the two-commit script only catches status transitions, not edits to an already-verified artifact.

Falsification statement

This release is wrong if, on either execution path, a one-hour position hold exceeds 1.0 m final horizontal error or 2.0 m peak horizontal excursion — the bars the nightly soak now enforces on both the native and wasm paths — or if the same hold, run on real 6X-RT silicon rather than the gz plant, shows the estimator diverging where the simulated plant does not. The second clause is the one this release cannot yet test: every number above comes from simulation, and no claim here has been measured on a vehicle.

Verification tracks at efc0dbf0ff04

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

Every per-commit track ran and passed on this commit.

track	workflow	on this commit
Tests ×3, Clippy, Format	ci.yml	✅ passed
Kani bounded model checking	kani.yml	✅ passed
Verus SMT proofs	verus.yml	✅ passed
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:

• #417 — the required gates can pass vacuously for a PR that touches only the shipped wasm components
• #546 — FV-FALCON-HOLD-001 checks HOLD-P01's bound on the FINAL sample only, then sets both mid-run aggregates at twice it (rms_steady < 1.0 vs a 0.5 m vertical bound, peak_horiz < 2.0 vs 1.0 m horizontal)
• #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

Release note — falcon-v1.140.0

9 artifact(s) in scope: 9 delivered, 0 withheld.

Functionalities provided

sw-req

• SWREQ-FALCON-BATTERY-P03 (verified) — BATTERY-P03 — a pack that stops REPORTING in flight shall raise the battery failsafe, not fly on
• SWREQ-FALCON-ENDURANCE-P01 (verified) — ENDURANCE-P01 — a position hold shall stay bounded for HOURS, not seconds, and be watched nightly
• SWREQ-FALCON-HOLD-P01 (verified) — HOLD-P01 — a stationary position hold shall stay bounded for at least 60 s, horizontally as well as vertically
• SWREQ-RELAY-MIXPROOF-P01 (verified) — MIXPROOF-P01 — the MIX-P06 priority-mix bound proof shall not depend on a solver's heavy tail

sw-verification

• FV-FALCON-BATTERY-003 (verified) — BATTERY-P03 — the lost-sense failsafe fires, and the test fails without it (v1.140)
• FV-FALCON-ENDURANCE-001 (verified) — ENDURANCE-P01 — a 12 h hold on a plant that can tilt, and a nightly job that measures it (v1.140)
• FV-FALCON-HOLD-001 (verified) — HOLD-P01 — the 5 Hz hold converges, on SimBackend and on the gz plant: 40 s → 300 s (v1.140)
• FV-RELAY-FLEET-002 (verified) — FLEET-P01 — starvation is measured from JOBS, and hosted contention is not reported as a dead fleet (v1.140)
• FV-RELAY-MIXPROOF-001 (verified) — MIXPROOF-P01 — the compositional MIX-P06 proof passes, can fail, and halves the instance (v1.140)

Limitations in relation to the committed scope

None — every artifact committed to falcon-v1.140.0 is release-ready.

Result of verification measures

5 of 9 delivered artifact(s) have NO verification evidence (neither a verifies link nor a source marker):

• FV-FALCON-BATTERY-003
• FV-FALCON-ENDURANCE-001
• FV-FALCON-HOLD-001
• FV-RELAY-FLEET-002
• FV-RELAY-MIXPROOF-001

Not covered by this note

Automotive SPICE 11-03 names these release-note elements. rivet does not yet compute them, so they are declared rather than omitted:

• application parameters — not modelled
• configurations and variants — the variant subsystem exists but is not wired in here
• intended area and environment of usage — not modelled
• impact to other components linked to the release — needs the cross-repo externals graph
• upstream or downstream compatibility — not modelled
• copyright and license information — the cargo-deny licenses gate produces this but it is not read here
• approval for delivery by responsible roles — rivet check review-signoff enforces it but emits no record (REQ-333)
• dependencies to other linked products — not modelled