This paper presents a comparative evaluation of three state-of-the-art neural network (NN) formal verification tools: α-CROWN, β-CROWN, and Marabou. We evaluate their performance with varying input perturbation magnitudes on an automated driving object detection task, which is a novelty in literature. The results reveal distinct trade-offs between computational efficiency and verification completeness: complete methods, such as β-CROWN and Marabou, provide definitive verification guarantees, with increased computational overhead, particularly for Marabou. α-CROWN is faster, but does not always achieve convergence, particularly in small-perturbation ranges. Interestingly, α-CROWN is able to detect all the constraint violations, which makes the method very useful despite its limitation. These findings provide key insights for selecting verification tools based on application requirements and computational constraints in safety-critical deep learning deployments.