Vehicle: An Open-Source Toolkit for Injecting Formal Verification Capabilities into Neural Networks

Vehicle is an open-source toolkit aimed at embedding logical specifications into neural networks, bridging the gap between deep learning and formal verification. Its core is a higher-order functional specification language, which supports compiling the same specification into training loss functions, verifier queries, and exporting to interactive theorem provers to achieve formal verification of neural networks. The project is maintained by the vehicle-lang team, with source code hosted on GitHub (link: https://github.com/vehicle-lang/vehicle), and was released on 2026-05-23. It addresses the "black box" dilemma of neural networks and provides credibility guarantees for AI systems in safety-critical domains such as autonomous driving and medical diagnosis.

Deep learning models have made breakthroughs in image recognition, NLP, autonomous driving, and other fields, but their decision-making processes are difficult to explain and verify. Traditional testing cannot cover all input scenarios, posing high risks in safety-critical domains. Formal verification ensures that systems meet specifications through mathematical proof, but the nonlinear nature of neural networks makes them difficult to describe using traditional logical frameworks, leading to significant challenges in application.

The core design philosophy of Vehicle is that the same specification can be reused across multiple stages of the neural network lifecycle: compiled into a training loss function to guide learning, compiled into a verifier query for pre-deployment verification, and exported to a theorem prover for system-level verification. Its specification language adopts a higher-order functional paradigm and supports dependent types, enabling concise expression of complex properties (e.g., monotonicity constraint: forall x y. x <= y => network(x) <= network(y)). The powerful type system can catch errors at compile time and ensure compatibility between specifications and network architectures. Related research was published at the CPP'23 conference.

Vehicle's technical implementation includes three parts: 1. Compile specifications into differentiable loss functions to achieve "specification-guided learning"; 2. Integrate Marabou (an SMT-based neural network verifier) to prove that the specification holds for all inputs or generate counterexamples; 3. Support exporting verification results to interactive theorem provers such as Agda, Rocq, and Isabelle to ensure the correctness of neural networks as system components. If network weights change, the proof check will fail, preventing the deployment of unverified models.

Vehicle provides several application cases: 1. ACAS Xu UAV collision avoidance system: Reproduce the specifications in the Reluplex paper to describe complex safety properties; 2. Automotive controller: Prove that the controller can keep the car on the road under sensor noise and crosswind interference; 3. MNIST robustness verification: Prove that the classifier is robust to small perturbations in the image neighborhood, and the classification result remains unchanged under adversarial sample attacks.

Vehicle seamlessly integrates with the existing deep learning ecosystem: It supports ONNX for model formats (compatible with PyTorch and TensorFlow); IDX for data formats (the standard format for MNIST); Marabou (an SMT-based verifier) as the verification backend; and interfaces with interactive theorem provers such as Agda, Rocq, and Isabelle.

Vehicle has a solid academic foundation: The tool paper was published in EPTCS/FSCD 2025, the type checker design was published at CPP'23, and the research on compiling to verifier queries is an arXiv 2024 preprint. The project is under active development, and the community is welcome to contribute via the GitHub Issue Tracker (e.g., adding support for new model formats, verifiers, or theorem provers). In the future, Vehicle will become a key technology for ensuring system credibility in the AI safety field, promoting the development of reliable and interpretable AI.