Abstract Research on neural network verification has traditionally emphasized scalability. However, recent invalidations of formally verified results of neural networks highlight soundness as an equally important goal. Pursuing inherent soundness, we present Rocq-NN-Roll , the first formally verified prover for rational-valued piecewise-affine neural networks. Rocq-NN-Roll combines a network and its specification, including hyperproperties, into a piecewise-affine function and reduces the verification task to solving linear inequalities over the network’s polyhedral regions. Developed in Rocq, the prover also provides the first automated proof support for neural networks within any interactive theorem prover, highlighting their still underexplored role in this field.

This paper presents the use of the Frama-C toolkit for the formal verification of a model of train-controlling software against the requirements of the CENELEC norm EN 50128. We also compare our formal approach with traditional unit testing.