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 `...

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

falcon-v1.138.0

falcon v1.138.0 — the wasm cascade flies Gazebo, and the 15-second swing is fixed

The published wasm cascade now flies real Gazebo, and the "it starts
swinging after about fifteen seconds" report is fixed at the root.

This bundles the v1.136 → v1.138 arc; those tags were never cut.

The swing

Reported from a Windows/WSL2 bench: "es fängt nach etwa 15 sekunden an zu
schwingen." Reproduced, and it is not drift — it is a limit cycle driven by the
altitude integral, which charged through the entire climb and then spent that
charge as overshoot (NED, negative is up):

t=7.9s   true_z -2.14  (target reached)    alt_int -6.26   <- peak charge
t=13.9   true_z -2.64  (overshoot)         alt_int -3.45
t=39.9   true_z -0.08  (nearly aground)    alt_int -5.72

At ki 0.03, ±6 is a ±0.19 thrust swing on a 0.585 hover. The integral now
charges only when the vehicle is not already converging.

Before: 0.62 m error at 16 s, and a 40 s hold ends near the ground. After: four
25 s holds measured 0.02, 0.04, 0.21 and 0.10 m — and alt_int sits at
−0.040 for the whole hold instead of swinging ±6. (Four runs rather than one
because a single green gz run has already fooled us once this cycle.)

Both obvious fixes were measured and rejected: a velocity gate cannot separate
the cases (the climb runs at only 0.1–0.29 m/s), and an error band cannot either
(the thrust-lapse sag the integral must reject is ~1.5 m, larger than the band
that would block the climb). Their product does separate them.

Also in this release

• configure(vehicle-config) — nine airframe values a host can install.
  Before it, every number was frozen inside the component and no host could
  correct them from outside.
• ESC telemetry on the seam — read_motor_rpm had no field at all, so the
  rotor-out FDI in the published component was inert by construction.
• Gazebo runs in CI for the first time, with video recorded every run and a
  hard gate on the hold error. The wasm and native paths are bit-identical
  per-motor across every tick.

---

Answers to two questions from the embedded track

1. "synth float poles are WIP (#708/#369). Was fehlt dafür noch?"

Those notes are stale, and floats lower fine. #369 (soft-float for all
f32/f64) and #708 (f32.load + i32.reinterpret_f32) were both closed
10–11 July 2026. Verified on synth 0.66.0, --target cortex-m7dp:

vmul.f32  s3, s0, s1
vadd.f32  s4, s3, s2
vdiv.f32  s2, s0, s1
vsqrt.f32 s1, s0

Real hardware FPU, hard-float ABI. So the trivial float path you asked us to
validate passes.

One warning that matters more than the answer

A stale synth silently emits wrong code. Our first attempt used a
four-month-old binary, which compiled the same module with exit 0 and
emitted:

export	emitted	meaning
faxpy(a,b,c)	mov r0,r2 ; bx lr	returns c — no multiply, no add
fdiv(a,b)	mov r0,r1 ; bx lr	returns b
fsqrt(x)	bx lr	returns x

No FPU instructions, no error, no warning. We nearly reported "floats don't
lower, your route stalls" on the strength of it. So your instinct to validate a
trivial float path is exactly right — and the first thing to validate is the
version. Pin synth through varve rather than a cargo install binary, and
disassemble the result once; an integer function of the same shape is a good
control (ours lowered to a correct mul.w/adds in 10 bytes while the float
one was 4).

What is actually still missing, for our cascade

On synth 0.66.0 / cortex-m7dp, 21 of the cascade's 22 functions lower,
including 1408- and 1468-byte ones. Exactly one declines — the tick itself:

GI-FPU-002: VFP register file exhausted (S0..S15 all live) — f32/f64 register
pressure exceeds the file; the backend retries with VFP spilling (#881) and
this surfaces only if that also fails

Target sensitivity, same input:

target	functions skipped of 22
cortex-m7dp	1 (the tick only)
cortex-m4f	3
cortex-m7	3
cortex-m3 (no FPU)	16

We tried reducing the pressure from our side by splitting the export into a
forwarder plus an #[inline(never)] body. It does not help — the decline
moves with the body, so the pressure is inherent to the tick (where
FlightCore::step inlines the whole cascade), not to the export boundary.
Filed as synth#1267, including the question of whether per-stage
#[inline(never)] in the guest is the intended remedy.

So: floats are not the blocker. Register pressure in one large tick is.
That is a much narrower risk than "the whole meld+synth route stalls", and it
is visible on day one exactly as you suggested.

Not validated here: the → Renode half. Renode is not installed on this
machine, so we confirmed synth compile --cortex-m only. Someone with Renode
should close that loop before the firmware rewrite goes on the schedule.

2. "Can synth emit a relocatable object or static archive, rather than a linked ELF?"

Yes — a relocatable object. synth compile --relocatable:

int_rel.o: ELF 32-bit LSB relocatable, ARM, EABI5 version 1 — not stripped
00000000 g     F .text  0000000a iaxpy

ET_REL, with global function symbols in .text that a linker can see. The
flag's own help is explicit: "Force relocatable object (.o, ET_REL) output even
when wasm has no imports — for linking into a host build system." --link is
the opposite direction (links to firmware ELF via arm-none-eabi-gcc), and
--builtins takes a kiln-builtins .o.

A static archive is not emitted directly — that is arm-none-eabi-ar rcs libfoo.a out.o. One gotcha we hit: use the cross ar. The macOS host ar
accepts the file and produces a malformed archive (ranlib: warning: archive member not a mach-o file).

So the PX4-module route is not gated on output format. It is gated on
GI-FPU-002 for the tick, above.

---

Known, filed, not fixed

• #403 — the horizontal loop diverges after ~26 s of hold; it was hidden
  under the altitude oscillation until that was fixed. This is why a 40 s hold
  still ends badly even though the altitude loop is now clean.
• #398 — rotor-out recovery does not hold on the gz plant.
• #397 — //:falcon-cascade has not built under Bazel since #393, so the
  cascade's witness MC/DC coverage is not being produced.
• synth#1267 — the cascade tick declines on cortex-m7dp.

Falsification

This release is wrong if a 25 s stationary 2 m hold on the gz falcon-quad,
driven by the published component through the Component Model seam, leaves the
vehicle more than 0.5 m from the commanded altitude — or if the wasm and native
paths ever differ by a single per-motor bit.

falcon-v1.135.0

What's Changed

• perf(cascade): measure the flight cascade — 1.2413 µs/tick, estimator is 91% (PERF-P01) by @avrabe in #361
• plan(roadmap): cut v1.135 around PERF-P01 alone; TRACE-P02 → v1.136 by @avrabe in #363

Full Changelog: falcon-v1.134.1...falcon-v1.135.0

falcon-v1.134.1

What's Changed

• fix(gate): the batching log said "2+ times" while the threshold is 5 by @avrabe in #358
• fix(oci): export __heap_base explicitly — v1.134.0 shipped without it by @avrabe in #359
• build(deps): bump taiki-e/install-action from 2.86.1 to 2.86.5 by @dependabot[bot] in #360

Full Changelog: falcon-v1.134.0...falcon-v1.134.1

falcon-v1.134.0

What's Changed

• feat(ci): detect fleet starvation — the failure mode is silence by @avrabe in #348
• fix(ci): give falcon-hello a per-run port pair — fixed ports collide by @avrabe in #349
• build(deps): bump taiki-e/install-action from 2.85.6 to 2.85.10 by @dependabot[bot] in #351
• feat(verify): census the whole-crate verification steps (weak evidence, #262) by @avrabe in #344
• verify(v1.133): record the release evidence — and why NOTHING is promoted yet by @avrabe in #347
• feat(oci): emit relocation metadata — meld REJECTED the v1.133 cascade (OCI-P05) by @avrabe in #352
• verify(oci): record the EXTENT half — .bss was invisible, not just relocs missing by @avrabe in #353
• plan(roadmap): cut v1.134 minimal — OCI-P05 alone; defer OCI-P03 + TRACE-P02 by @avrabe in #354
• build(deps): bump taiki-e/install-action from 2.85.10 to 2.86.1 by @dependabot[bot] in #356
• perf(gate): batch per-crate — one cargo run instead of 67 (#350) by @avrabe in #357
• feat(oci): tune per-stage shadow stacks (OCI-P06) — and unskip the verifiers that never ran by @avrabe in #355

Full Changelog: falcon-v1.133.0...falcon-v1.134.0

falcon-v1.133.0

What's Changed

• plan(roadmap): scope v1.132–v1.135 in rivet by @avrabe in #334
• feat(trace): backfill the per-artifact release assignment (TRACE-P01, v1.132) by @avrabe in #335
• feat(oci): publish under the nested path ghcr.io//falcon/ by @avrabe in #338
• feat(wit): rename the WIT namespace falcon:* → pulseengine:falcon-* (OCI-P04) by @avrabe in #337
• plan(roadmap): defer TRACE-P02 to v1.134 — v1.133 is the OCI/release arc by @avrabe in #341
• feat(oci): convert the whole cascade to no_std — WASI-free, no-grow (OCI-P02) by @avrabe in #339
• build(deps): bump wit-bindgen from 0.59.0 to 0.60.0 by @dependabot[bot] in #317
• feat(release): create the release as a DRAFT, publish only after the guard (REL-P01) by @avrabe in #340
• verify(v1.133): close the V — REL-P01, OCI-P02 and OCI-P04 had zero verifiers by @avrabe in #346

Full Changelog: falcon-v1.131.1...falcon-v1.133.0

falcon-v1.131.1

What's Changed

• fix(release): install wasm32-unknown-unknown — v1.131.0 shipped without components by @avrabe in #332

Full Changelog: falcon-v1.131.0...falcon-v1.131.1

falcon-v1.131.0

Warning

SUPERSEDED BY falcon-v1.131.1 — THIS RELEASE IS INCOMPLETE.

The Wasm component assets are missing from this release, and no components were published to ghcr for 1.131.0. The flight-component job failed on a missing rustc target (wasm32-unknown-unknown, fixed in #332) after the GitHub Release had already been created.

Nothing incorrect was published — the build aborted rather than bundling a stale artifact, and the OCI push was skipped, so ghcr.io/pulseengine/falcon-* served only 1.129.0/1.130.0. This release is incomplete, not wrong.

Use falcon-v1.131.1, which carries the same changes plus the fix. The publish-before-components ordering that allowed a partial release to go public is tracked in #333.## What's Changed

• build(deps): bump taiki-e/install-action from 2 to 2.85.6 by @dependabot[bot] in #326
• fix(rate): bounded arena instead of a growing allocator — remove memory.grow by @avrabe in #327
• feat(build): build no_std components for wasm32-unknown-unknown, not wasip2 by @avrabe in #329
• feat(oci): set OCI manifest annotations so wasm.directory listings aren't bare by @avrabe in #328
• verify(oci): record the v1.131 no-grow + annotations evidence; defer P06 by @avrabe in #331

Full Changelog: falcon-v1.130.0...falcon-v1.131.0

falcon-v1.130.0

What's Changed

• fix(oci): falcon-rate shipped as a core module — export cabi_realloc, fail loud, assert the header by @avrabe in #323
• fix(build): de-conflate std from bazel-bindings; select artifacts by name; register components by @avrabe in #324
• verify(oci): record the field-found evidence gap; defer P06 to v1.131 by @avrabe in #325

Full Changelog: falcon-v1.129.0...falcon-v1.130.0