Control-code verification | Mergen Ulziibayar

Numerical qualification and synthetic development campaign

Completed 6,144 randomized development traces, covering 1,572,864 steps with zero numerical-bound violations. The campaign also identified 8,316 exact-versus-rounded branch-difference steps.

Holybro X500 kit with a Pixhawk 4 controller, from the PX4 documentation. Platform reference photograph.Credit: PX4 documentation contributors. CC BY 4.0. Image reproduced unchanged.Full-size image Image source

results and contributions

Randomized development traces	6,144
Exact-covered development steps	1,572,864
Numerical-bound violations	0 in this campaign
Exact / rounded branch differences	8,316 steps across 1,016 traces

Repository Numerical result at source commit Current roadmap PX4 predecessor and scoped results Randomized campaign counts Numerical admission and review scope

figures and hardware

Open any image at full size. Source links identify the retained revision.

**Numerical development result.** Compiled trajectories and errors against exact intent. Dashed bounds are deterministic error bounds, not confidence intervals.Full-size image Image source

**Scoped predecessor result.** PX4 component comparisons on directed and random input sequences.Full-size image Image source

**SITL development observations.** Datalink-loss observations from development runs. Timer settings and observed action timing are distinct quantities.Full-size image Image source

design evolution

The design and analysis steps that produced the current work.

Work	Engineering question	Approach	Outcome
PX4 failsafe predecessor	Agreement with the firmware was limited to selected states and inputs.	Compare the Python model with the compiled PX4 class on identical sequences.	The initial 11 directed sequences agree after an update-order fix. Later model and adapter repairs resolved 495 disagreements in 1,500 development sequences; all 1,000 fresh reserved sequences agree within the declared domain.
Generated-code successor	A passing check covers only its represented boundary.	Separate exact intent, binary32 semantics and compiled output.	Numerical development traces agree within the declared bounds.
Development campaign and review	Separate value accuracy from branch semantics and compiler behavior.	Retain exact and rounded histories, minimized cases and an ARM Linux GCC/QEMU comparison.	Qualified the next-state value claim after scoped Claude AI technical review; preserved signed-zero and reverse-slew findings.

methods and scope

Numerical admission covers next-state values in the declared domain, strict arithmetic and up to 256 steps since reset. Branch differences compare exact intent with rounded computation; they are not C translation failures. The separate pilot retains a signed-zero mismatch. No LLM translation campaign, PX4 wrapper qualification or flight validation is claimed. Steps within a trace are dependent.

project record

Evidence	Numerical qualification and synthetic development campaign
Status	In Progress
Timeline	2026
Role	Numerical specification, generated-code qualification and differential checks
Tools	Python, CasADi, Clang, C, GitHub Actions

← All projects