ABSTRACT. Large Language Models (LLMs) are increasingly integrated into organizational workflows, raising growing concerns about their potential abuse for fraud, security breaches, or intellectual property leakage. While LLMs embed protective mechanisms and organizations develop their own guardrails, many practical guardrail approaches remain stateless and lack formal temporal semantics, and existing formal methods are often domain-specific or rely on structured event representations. We propose a runtime verification (RV) framework that treats an LLM conversation as an execution trace that can be formally verified and develop a corresponding tool called Temporal Guard. It observes the stream of user messages and LLM-generated assistant responses, grounds each message into a set of atomic propositions, and thereby constructs a Boolean-labeled trace. Safety policies are specified as formulas in past-time linear temporal logic, and the monitor checks the evolving Boolean trace online to decide whether the conversation satisfies the policy. The central challenge is grounding: bridging the gap between the precise Boolean semantics of temporal logic and the ambiguity of natural language utterances. To address this, we developed a semantic grounding layer and experimentally evaluated a range of grounding strategies, including an embedding-based approach, Natural Language Inference (NLI), and LLM-based zero/few-shot classification. We demonstrate the effectiveness of Temporal Guard through grounding and end-to-end monitoring experiments.

ABSTRACT. Mixture-of-experts (MoE) architectures offer modularity and scalability, yet their robustness, and the practicality of certifying that robustness, in heterogeneous settings are not well understood. This work presents MetaMoE, a heterogeneous MoE framework designed for compositional formal verification. In MetaMoE, a neural network, called a router, classifies an input image's domain and routes it to the corresponding domain expert neural network for fine-grained classification; we study how robustness propagates compositionally across these router and experts and establish when system-level verification can be derived from component-level verification. In homogeneous MoE, all experts share the same task, so a misroute may still preserve correctness if the receiving expert classifies the input correctly; in heterogeneous MoE, experts operate on disjoint class spaces, making any misroute catastrophic. We prove that when the router maintains expert selection under hard routing (k=1) within a perturbation limit, and the selected expert also maintains its classification within that perturbation limit, the end-to-end system robustness is compositional. This enables scalability as the computational power needed for verification and re-verification does not snowball as the system expands. We further complement the formal verification results with empirical experiments, which support the same robustness trends observed under certification. Experiments across 8 MoE configurations and 3 perturbation budgets show that robustly trained (RT) experts improve adversarial accuracy by up to 13.1% over non-robustly trained (NRT) ones and are a prerequisite for formal certifiability -- NRT models on complex domains are completely unverifiable -- while router training paradigm has negligible impact (<0.1%), and verified routers achieve 100% certified robustness accuracy (RoCRA) at practical perturbation bounds. These results outline a principled path toward scalable, verifiable modular AI.

ABSTRACT. Probabilistic verification problems of neural networks are concerned with formally analysing the output distribution of a neural network under a probability distribution of the inputs. Examples of probabilistic verification problems include verifying the demographic parity fairness notion or quantifying the safety of a neural network. We present a new algorithm for solving probabilistic verification problems of neural networks based on an algorithm for computing and iteratively refining lower and upper bounds on probabilities over the outputs of a neural network. By applying state-of-the-art bound propagation and branch and bound techniques from non-probabilistic neural network verification, our algorithm significantly outpaces existing probabilistic verification algorithms, reducing solving times for various benchmarks from the literature from tens of minutes to tens of seconds. Furthermore, our algorithm compares favourably even to dedicated algorithms for restricted probabilistic verification problems. We complement our empirical evaluation with a theoretical analysis, proving that our algorithm is sound and, under mildly re- strictive conditions, also complete when using a suitable set of heuristics.

ABSTRACT. Autonomous systems operating in the real world encounter a range of uncertainties. Probabilistic neural Lyapunov certification is a powerful approach to proving safety of nonlinear stochastic dynamical systems. When faced with changes beyond the modeled uncertainties, e.g., unidentified obstacles, probabilistic certificates must be transferred to the new system dynamics. However, even when the changes are localized in a known part of the state space, state-of-the-art requires complete re-certification, which is particularly costly for neural certificates. We introduce VeRecycle, the first framework to formally reclaim guarantees for discrete-time stochastic dynamical systems. VeRecycle efficiently reuses probabilistic certificates when the system dynamics deviate only in a given subset of states. We present a general theoretical justification and algorithmic implementation. Our experimental evaluation shows scenarios where VeRecycle both saves significant computational effort and achieves competitive probabilistic guarantees in compositional neural control.

ABSTRACT. Current Deep Neural Network (DNN) verifiers are typically designed to prioritize scalability over reliability. Reliability can be reinforced through the generation of proofs that are checkable by trusted, external proof checkers. To date, only a handful of verifiers support proof production; and these rely on verifier-specific formats, and balance between scalability, proof detail, and the trustworthiness of their proof checker. In this tool paper, we introduce PICID, a DNN verifier that produces proofs in the standard Alethe format for SMT solving, checkable by multiple existing checkers. PICID implements a parallel CDCL(T) architecture that integrates a state-of-the-art, proof-producing SAT solver with the Marabou DNN verifier. Furthermore, PICID leverages UNSAT proofs to derive conflict clauses. Our evaluation shows that PICID generates valid proofs in the vast majority of cases and significantly outperforms existing tools that produce comparable proofs.

ABSTRACT. Formal verification of transformers has become increasingly important due to their widespread deployment in safety-critical applications. Compared to classic neural networks, the inferences of transformers involve highly complex computations, such as dot products in self-attention layers, rendering their verification extremely difficult. Existing approaches explored over-approximation methods by constructing convex constraints to bound the output ranges of transformers, which can achieve high efficiency. However, they may sacrifice verification precision, and consequently introduce significant approximation error that leads to frequent occurrences of false alarms. In this paper, we propose a transformer verification approach that can achieve improved precision. At the core of our approach is a novel usage of ReLU, by which we represent a precise but non-linear bound for dot products such that we can further exploit the rich body of literature for convex relaxation of ReLU to derive precise bounds. We extend two classic approaches to the context of transformers, a rule-based one and an optimization-based one, resulting in two new frameworks for efficient and precise verification. We evaluate our approaches on different model architectures and robustness properties derived from two datasets about sentiment analysis, and compare with the state-of-the-art baseline approach. Compared to the baseline, our approach can achieve significant precision improvement for most of the verification tasks with acceptable compromise of efficiency, which demonstrates the effectiveness of our approach.

ABSTRACT. The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network's non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.

ABSTRACT. Safety-critical deployment of machine learning models requires unambiguous specification and verified implementation of tensor operators. This paper presents a formally verified pipeline based on the Why3 deductive verification platform. The pipeline takes each operator from an abstract WhyML specification over mathematical tensors to extracted C code, via a concrete implementation on flat arrays linked by a machine-checked refinement proof. A reusable library supports the development, providing abstract tensor types, a row-major layout with proven bijectivity, and a refinement mapping to a C-level representation. We illustrate the workflow on several ONNX operators, developed within the SONNX Working Group. Finally, we demonstrate how the abstract specifications compose to enable contract-based verification of functional properties of complete networks. The methodology is applicable beyond ONNX to any framework requiring verified tensor implementations.

ABSTRACT. Graph neural networks (GNNs) have become a prominent approach for developing fast, topology-aware surrogates in electric power systems, supporting tasks such as power flow (PF) analysis, optimal power flow (OPF) estimation, and cascading failure analysis (CFA). Despite this growing use, formally verifying GNN-based models remains challenging, with existing methods limited in scope. We extend the neural network verification (NNV) framework to graph-structured inputs through GraphStar sets, a generalization of Star sets that captures uncertainty over both node and edge features. This extension enables the propagation of linear message-passing operations and the sound approximation of ReLU nonlinearities for GNN architectures, including graph convolutional network (GCN) and graph isomorphism network with edge features (GINE) layers. We evaluate GNNV across three power system tasks, PF, OPF, and CFA, on the IEEE-24, IEEE-39, and IEEE-118 test cases, as well as two standard graph classification benchmarks, ENZYMES and PROTEINS. Our results show that GNNV provides tighter robustness guarantees than CORA on graph classification models with ReLU-based activations and, for the first time, delivers edge-aware robustness guarantees for GINE-based PF and OPF models under joint node and edge perturbations.

ABSTRACT. Vision-Language Models (VLMs) struggle with explainability and tasks requiring step-by-step reasoning. This paper proposes a neuro-symbolic framework that leverages both logic and neural networks for interpretable results; chaining together convolutional neural networks (CNNs), computer vision techniques, and Satisfiability Modulo Theories (SMT). We introduce a challenging benchmark suite of KenKen and Sudoku puzzles, both NP-complete in the general case. Provided with an unsolved board image, these puzzles require image decomposition, constraint evaluation, and error detection/correction, making it a relevant benchmark suite for VLMs. We compare our neuro-symbolic framework against five state-of-the-art VLMs: Gemini-2.5-Pro, GPT-4o, GPT-4o-mini, Claude Sonnet 4.0, and Qwen2.5-VL-7B-Instruct. These VLMs have significant difficulty solving Sudoku or KenKen puzzles beyond 4x4 grids. The neuro-symbolic framework achieves 100% accuracy on computer-generated characters for all classes. For handwritten characters, we demonstrate the neuro-symbolic can correct image decomposition errors, improving solve rate. Overall, the benchmark is used to demonstrate the neuro-symbolic framework outperforms state-of-the-art VLMs while providing explainable reasoning to enable the self-correction of error. The benchmark suite consists of 2200 board images: seven classes of KenKen puzzle and four classes of Sudoku, for both computer-generated and handwritten characters.

ABSTRACT. While neural networks have achieved remarkable success across a wide range of application domains, their predictions remain brittle when confronted with adversarial perturbations. To enable their responsible deployment in safety-critical settings, neural network verification techniques have been developed to formally establish input–output properties of interest. However, even state-of-the-art verification systems such as α,β-CROWN, the winner of the Verification of Neural Networks Competition (VNN-COMP) since 2021, may fail to prove challenging properties within reasonable time budgets. Fully exploiting the capabilities of such systems typically demands careful tuning of numerous parameters, a process that often relies on substantial domain expertise and extensive manual experimentation. In this work, for the first time, we apply automated algorithm configuration to α,β-CROWN using SMAC3, thereby eliminating the need for labour-intensive manual tuning. We show that, given a carefully designed parameter search space, automatically discovered configurations can achieve performance comparable to expert-crafted configurations, even when using relatively modest computational budgets for the optimisation process. We evaluate our approach on the benchmarks from the regular track of VNN-COMP 2025 and demonstrate that the automatically configured version of α,β-CROWN achieves a higher overall score than the author-provided configuration when applying the scoring scheme of the competition.

ABSTRACT. With AI increasingly deployed in safety-critical systems, providing formal robustness guarantees for the underlying models is essential. Existing verification methods either rely on overly conservative approximations or incur prohibitive computational costs. For example, the use of $\ell_p$-norm perturbations in video settings encodes the belief that the adversary can inject noise in every video frame. In practice, adversarial perturbations exhibit structured spatial and temporal correlations, constrained to lower-dimensional, semantically meaningful subspaces. In this work, we study robustness verification of \emph{3D convolutional neural networks} (3D CNNs) processing video and volumetric inputs, targeting applications in action recognition (UCF-101), autonomous driving (Udacity), and medical imaging (MedMNIST) exploiting realistic assumptions on adversarial strength by modelling them as spatio-temporal constraints --- where the attacker can modify either a subset of frames or patches within a set of consecutive frames. We demonstrate that modelling realistic constraints enables tighter approximations, particularly in CNNs. We introduce \emph{Spatio-Temporal Bound Propagation} (STBP), a verification framework that computes an exact closed-form characterization of the first convolutional layer and propagates certified bounds through subsequent layers using scalable approximations. Computing the exact closed-form provides the tightest bounds for the first convolutional layer. Thus, we utilise approximation methods in the remainder of the network. To spur further progress in this field, we propose \texttt{ST-Bench}, a verification benchmark for autonomous driving and activity recognition, to systematically evaluate verifiable robustness. Compared to existing verification and training-based approaches, STBP provides stronger robustness guarantees with significantly improved scalability, achieving up to $1.7\times$ higher certified robust accuracy under identical perturbation budgets.