Published OCI components advertise "Formally-verified geometric SO(3)" while wrapping the unverified legacy PID controller

[avrabe]

The claim

wasm/cm/attitude/Cargo.toml:5

description = "Formally-verified geometric SO(3) attitude controller as a WebAssembly Component — attitude setpoint + vehicle state → body-rate setpoint."

release.yml:610,614 pipes that string verbatim into
org.opencontainers.image.description — it is what ghcr.io and wasm.directory
render to anyone browsing the package. docs/OCI-DISTRIBUTION.md:19 repeats it.

Both halves are false

"geometric SO(3)" — the component depends on relay-att
(wasm/cm/attitude/Cargo.toml:21), whose own header reads:

crates/relay-att/plain/src/lib.rs:1
//! Relay attitude controller — quaternion-error proportional control.

The actual geometric SE(3) controller is relay-geo, which exists explicitly to
replace this one. The component wraps the controller falcon-core dropped on
2026-06-03.

"Formally-verified" — relay-att has no verification of either kind:

$ grep -c 'relay-att' .github/workflows/kani.yml     → 0
$ grep -c 'relay_att_verus_test' BUILD.bazel          → 0

No Kani matrix entry, no Verus target. The crates that are verified —
relay-adrc, relay-geo — are wrapped by no published component at all.

The same applies to wasm/cm/position (relay-pos) and wasm/cm/rate
(relay-rate); all three are in release.yml:573's
SLUGS="flight iekf position attitude rate mixer" and are pushed to ghcr and
cosign-signed by digest.

Why this one is worse than an internal inconsistency

This is the text an external integrator reads before pulling. A partner doing
wkg oci pull ghcr.io/pulseengine/falcon/attitude gets a signed artifact whose
registry metadata claims the modern, verified control law and delivers the
legacy, unverified one. The signature attests the bytes, not the description.

And note which component is absent from SLUGS: cascade — the one that
was actually fixed. The registry serves the drifted stack and not the repaired
one.

Fix directions

Short term: correct the descriptions to say what each component actually wraps,
and drop "Formally-verified" where no proof target exists. Medium term: decide
whether these three components should exist at all now that the cascade is the
flight core, and if they should, publish cascade too.

A description that asserts a verification status should be checkable — the
dependency audit could assert that any component claiming "Formally-verified"
wraps a crate with a Kani matrix entry or a verus_test target.

Falsification

Wrong if relay-att has a Kani matrix entry or a Verus proof target, or if
wasm/cm/attitude wraps relay-geo.