Compositional Formal Verification of Anti-Lock Braking System Neural Controllers

We present a compositional formal verification framework that establishes floating-point correctness and control safety for anti-lock braking system (ABS) neural controllers, using Rocq and Flocq as a single verification toolchain. We decompose the verification into three independent components. First, a Flocq proof bounds each binary32 operation to machine epsilon. Second, a CoqInterval-verified barrier certificate enforces eight pointwise conditions across four road surfaces, keeping the slip ratio within [0.03, 0.40]. Third, an ODE forward invariance lemma lifts these pointwise conditions to a temporal guarantee via the suprema axiom and ε-δ continuity arguments. The compositional theorem combines all three layers into an end-to-end safety proof. Our Rocq development (866 lines, 7 modules) compiles successfully: the core floating-point lemmas are Qed, with one lemma remaining Admitted. Numerical simulation across four road surfaces (after 0.3 s settling, v≥1.5 m/s) shows that the neural network controller achieves 100% closed-loop safety on every surface, including ice, outperforming the classical finite state machine controller (96.0–100%). The framework demonstrates that single-toolchain compositional verification of floating-point neural controllers is feasible, directly supporting ISO 26262 certification for safety-critical automotive systems. The verified barrier windows and open-source Rocq artifacts provide a reusable foundation for future neural ABS verification work.