blog(one-ulp): "One ulp of doubt" — the f32/f64 verification story

[avrabe]

Adds content/blog/2026-07-22-one-ulp-of-doubt.md — an engineering-notes post on the Falcon floating-point work (falcon-v1.123 → v1.127).

The story: a colleague asks whether the flight-control floats should be 32- or 64-bit; the honest answer is that 32-bit is the requirement (the M4's FPv4-SP has no f64 hardware — matching PX4/ArduPilot), but it was tribal knowledge. Three tiers of assurance follow, each catching what the last missed:

1. A CI gate enforcing f32 discipline — and Kani rejecting our first covariance floor because +∞ escaped a naive check.
2. An exhaustive sweep — all ~2.2 billion in-envelope f32 vs an f64 reference — finding the worst case (and the near-zero ulp artifact) the 4M-point sample had hidden.
3. A machine-checked proof — Gappa → Flocq → coqc, tight at 2⁻²⁴, non-vacuous (rejects 2⁻²⁵), a required gate.

Keeps the section most write-ups omit: what we did not prove (the Coq-Interval approximation layer, the reduction cancellation) and the notch fragility the kernel merely revealed — because that honesty is the point.

• Follows CONTRIBUTING: +++ TOML frontmatter, {% insight() %} opener, {% note() %} callouts, ## headings for the auto-TOC.
• draft = true, ready = false — private draft, held from autopublish; flip when you want it live.
• zola build passes locally; the only broken external links zola check reports are pre-existing in other posts, none in this one.
• Authored in a worktree off origin/main so no other in-progress branch was touched.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG