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.