ABSTRACT. Neural networks hold great potential to act as approximate models of nonlinear dynamical systems, with the resulting neural approximations enabling verification and control of such systems. However, in safety-critical contexts, the use of neural approximations requires formal bounds on their closeness to the underlying system. To address this fundamental challenge, we propose a novel, adaptive, and parallelizable verification method based on certified first-order models. Our approach provides formal error bounds on the neural approximations of dynamical systems, allowing them to be safely employed as surrogates by interpreting the error bound as bounded disturbances acting on the approximated dynamics. We demonstrate the effectiveness and scalability of our method on a range of established benchmarks from the literature, showing that it significantly outperforms the state-of-the-art. Furthermore, we show that our framework can successfully address additional scenarios previously intractable for existing methods -- neural network compression and an autoencoder-based deep learning architecture for learning Koopman operators for the purpose of trajectory prediction.

ABSTRACT. The specification and verification of temporal properties is crucial to assess the safety of monitoring systems. Said systems need to ensure that certain properties are validated during its full operation time. The rich pattern-finding capabilities of deep learning are a strong incitation to implement such monitors as neural networks. However, neural networks verification historically focused on properties related to a single point in time. In this paper, we present a way to encode Linear Temporal Logic (LTL) properties in a neural network specification language. We derive from this encoding an automated translation to existing off-the-shelf provers. We apply our system to the verification of an industrial use case: a monitoring system for batch distillation. We were able to successfully specify and verify most of the properties in a small runtime.

ABSTRACT. Neural network controllers for autonomous decision-making are well-established in cyber-physical systems, yet their deployment in safety-critical healthcare settings remains largely unverified. This paper presents a methodology and case study for the formal verification of a neural network controller for antibiotic dosing, motivated by the challenge of systems that must be simultaneously adaptive and provably safe across unbounded time horizons. We construct a simplified yet clinically-interpretable model that tracks drug concentration, body temperature, and white blood cell count. Vancomycin is selected as a representative antibiotic, widely prescribed for severe infections yet carrying a narrow therapeutic window, where supratherapeutic concentrations risk nephrotoxicity and subtherapeutic dosing risks treatment failure. A supervised neural network controller is trained on synthetic clinician-style dosing data. We establish formal verification of input-output safety properties, specifically verifying a property of a neural network that implies an infinite-horizon proof that automated dosing never exceeds the supratherapeutic boundary. This system property is proven in Rocq using the Vehicle interactive theorem prover backend to integrate the different proof systems. The end result is a verification pipeline that allows for a wide variety of treatment approaches whilst maintaining safety for each specific patient.

ABSTRACT. We present our ongoing work on the veriFIRE project: a collaboration between industry and academia, aimed at applying verification to increase the reliability of a real-world, safety-critical system. The system we target is an airborne platform for wildfire detection, which incorporates two deep neural networks. We present an end-to-end methodology for verifying consistency properties of this system. Our approach encodes application-grounded requirements into solver-compatible queries for existing neural network verifiers. We study properties of interest over critical operational scenarios: (i) monotonicity of detector confidence as target intensity increases; and (ii) bounded detector response under physically plausible blur over the sensor. We instantiate these encodings using state-of-the-art neural network verification backends and evaluate them at scale on real background samples. For the first property, all verification queries are solved in under five minutes. For the second property, verification is substantially harder, highlighting key scalability challenges for richer, higher-dimensional specifications. Overall, the results demonstrate that meaningful, domain-specific guarantees can be obtained for industrial systems.

ABSTRACT. Translating human-written mathematical theorems and proofs from natural language (NL) into formal languages (FLs) like Lean 4 has long been a significant challenge for AI. Most state-of-the-art methods either focus on theorem-only NL-to-FL auto-formalization or on FL proof synthesis from FL theorems. In practice, auto-formalization of both theorem and proof still requires human intervention, as seen in AlphaProof’s silver-medal performance at the 2024 IMO, where problem statements were manually translated before automated proof synthesis. We present ProofBridge, a unified framework for automatically translating entire NL theorems and proofs into Lean 4. At its core is a joint embedding model that aligns NL and FL (NL-FL) theorem+proof pairs in a shared semantic space, enabling cross-modal retrieval of semantically relevant FL examples to guide translation. ProofBridge integrates retrieval-augmented fine-tuning with iterative proof repair, leveraging Lean’s type checker and semantic equivalence feedback to ensure both syntactic correctness and semantic fidelity. Experiments show substantial improvements in proof auto-formalization over strong baselines (including GPT-5, Gemini-2.5, Kimina-Prover, DeepSeek-Prover), with our retrieval-augmented approach yielding significant gains in semantic correctness (SC, via proving bi-directional equivalence) and type correctness (TC, via type-checking theorem+proof) across pass@k metrics on miniF2F-Test-PF, a dataset we curated. In particular, ProofBridge improves cross-modal retrieval quality by up to 3.28x Recall@1 over all-MiniLM-L6-v2, and achieves +31.14% SC and +1.64% TC (pass@32) compared to the baseline Kimina-Prover-RL-1.7B.

ABSTRACT. As neural networks (NNs) become increasingly prevalent in safety-critical neural network-controlled cyber-physical systems (NNCSs), formally guaranteeing their safety becomes crucial. For these systems, safety must be ensured throughout their entire operation, necessitating infinite-time horizon verification. To verify the infinite-time horizon safety of NNCSs, recent approaches leverage Differential Dynamic Logic (dL). However, these dL-based guarantees rely on idealized, real-valued NN semantics and fail to account for roundoff errors introduced by finite-precision implementations. This paper bridges the gap between theoretical guarantees and real-world implementations by incorporating robustness under finite-precision perturbations --- in sensing, actuation, and computation --- into the safety verification. We model the problem as a hybrid game between a good Demon, responsible for control actions, and a bad Angel, introducing perturbations. This formulation enables formal proofs of robustness w.r.t. a given (bounded) perturbation. Leveraging this bound, we employ state-of-the-art mixed-precision fixed-point tuners to synthesize sound and efficient implementations, thus providing a complete end-to-end solution. We evaluate our approach on case studies from the automotive and aeronautics domains, producing efficient NN implementations with rigorous infinite-time horizon safety guarantees.

ABSTRACT. The rise in popularity and deployment of deep neural networks has resulted in an increased demand for trustworthy models, particularly in safety-critical applications. As a result, several solvers that formally verify properties of neural networks have been developed. However, state of the art solvers have combinatorially large configuration spaces. The task of selecting the best configuration for an instance or benchmark is non-trivial. Furthermore, current methods for algorithm selection and algorithm configuration are insufficient for large configuration spaces. We present REGENT, an automated selection tool for verification of neural network (VNN) solver configurations via Large Language Model (LLM) prompting. Our zero-shot selection method is a three stage LLM inference tool that takes as input a feature description of a VNN instance and outputs a solver configuration. In case of failure, feedback from the solver is passed back to the LLM, after which a new configuration is queried. Our reinforcement learning with optimization feedback (RLOF) method fine-tunes LLMs to output configurations that cause VNN solvers to improve on an optimization objective. We perform extensive empirical evaluations that show that the configurations selected by REGENT achieve comparable performance to hand-tuned configurations on a large set of competition grade test instances. When applying our fine-tuning approach, we show that LLMs can configure solvers to prove tighter bounds than those proven using hand-tuned configurations on up to 58% of the most challenging test instances. REGENT allows non-expert users of VNN solvers to automatically generate significantly better configurations, and therefore can save several human hours involved in hyperparameter-tuning.

ABSTRACT. Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of $\omega$-regular properties (and therefore linear temporal logic) over general state spaces, encompassing both countably infinite and continuous state spaces. Conversely, reinforcement learning (RL) methods for $\omega$-regular tasks have received considerable attention, but they typically lack formal guarantees that the learned policy satisfies the specification, except possibly for finite state and action spaces. We bridge these two lines of research by establishing a novel theoretical connection: under an appropriate reward, the value function associated to a policy that almost surely satisfies an $\omega$-regular property encodes a Streett supermartingale certificate for that specification. Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.

ABSTRACT. Neural networks (NN) are often represented using the Open Neural Network Exchange (ONNX) format that provides a rich set of operators. This richness implies that many tools support only a subset of ONNX operators and, consequently, a subset of NNs. However, some of these operators can be expressed equivalently as combinations of simpler, already supported, operators. In this work, we present an extension of CAISAR---a platform for verification of NN that uses external solvers---that automatically transforms these redundant operators into simpler ones before calling existing solvers, thus extending the range of these solvers. This work focuses on the argmax operator, proposing a transformation, proving its correctness, and presenting experimental results.

ABSTRACT. Safety analysis of neural-network controllers for cyber-physical systems requires combining closed-loop dynamical reasoning with formal neural-network verification. Standard invariant-based workflows typically compute the maximal controlled-invariant set before controller checking, although a violating execution may be detectable for an invariant inner-approximation. This paper proposes an incremental workflow for checking controller safe-set preservation. Starting from an initial inner-approximation, the method interleaves invariant refinement with verification, reuses proof results, checks only the newly added region between successive iterates, and supports early termination with a counterexample. If no violation is found, the verified domain grows progressively with each refinement step. Case studies on adaptive-cruise and lane-keeping neural controllers show that interleaving reduces time to counterexample in unsafe cases, lowers runtime in safe cases, and proof reuse becomes more beneficial as verification cost increases.

ABSTRACT. Markov Decision Processes (MDPs) are a powerful modeling paradigm for sequential decision-making problems, e.g., robot navigation and game playing. Decades of research have produced highly efficient algorithms for solving MDPs. A common limitation, however, is that the solutions (policies) are typically represented as large lookup tables that map agents' actions to thousands or even millions of states. In this work, we present a fast approach to optimizing (fixed-size) decision tree policies for MDPs, which are easier for human experts to analyze and for specialized tools to verify. Previous work tackled this problem using computationally intensive techniques, such as integer programming or abstraction refinement. While our method, Lipa, which combines branch-and-bound with smart heuristics, can often find high-quality policies orders of magnitude faster and prove optimality where previous methods fail. We evaluate Lipa on 21 discounted-return and model-checking benchmark MDPs of varying sizes and demonstrate consistent, significant improvement over the state of the art.

ABSTRACT. Counterfactual explanations (CEs) provide a simple, yet powerful interpretive approach to understanding neural network behavior, envisioning hypothetical scenarios by systematically altering input features and analyzing the resulting changes in model predictions. However, CEs are useful only if they are robust, i.e., they remain consistent and meaningful even when adversarially perturbed. While prior work has explored the development of generators for robust CEs, checking the robustness of CEs produced for DNNs has not been explored within the verification context, nor has it been studied under adversarial training. We present a systematic study utilizing adversarial training to fortify the underlying neural network, observing its effect on the formal robustness of DNNs with respect to CEs using α, β-CROWN, a state-of-the-art NNV. Our experiments across multiple datasets, network architectures, and CE generators indicate that adversarial training has a positive impact on the number of formally verified robust CEs. We also measure the impact of adversarial training on other desirable properties of CEs, such as plausibility and proximity. While plausibility does not change, there is a trade-off with proximity when using a gradient-based CE generator.