Lakhasly

3.14 Tools, Frameworks, and Verification Workflows Overview of Neural Network Verification Tools Neural network verification tools analyze whether neural networks satisfy properties such as safety and robustness.Combining formal verification with systematic testing, risk management, and continuous monitoring could strengthen the technical evidence supporting certification.The authors implemented a prototype Neuro-Symbolic Verifier (NSV) based on the Marabou verification framework and evaluated it using neural networks trained on the MNIST handwritten-digit dataset and the German Traffic Sign Recognition Benchmark (GTSRB).Standardized benchmarks, such as those used in the International Verification of Neural Networks Competition (VNN-COMP), facilitate more consistent comparisons by using common network and specification formats and controlled evaluation conditions However, comparative studies show that verification performance depends on the characteristics of individual problem instances.The authors reported that the integration of structured requirements management, technical evaluation methods, and automated MLOps workflows supports traceability, reproducibility, and the systematic assessment of trustworthy AI objectives.Evaluation Metrics, Benchmark Datasets, and Experimental Design Liu et al. (2024) evaluated their NARv approach using verification time, the number of successfully verified properties, and the sizes of abstract and refined neural networks.Xie et al. (2022) proposed a neuro-symbolic verification framework that addresses a limitation of traditional neural network verification methods, which mainly support properties expressed as logical constraints over network inputs and outputs.Their method uses Property Specification Patterns (PSP) to generate formal properties and observer automata, while Property Adaptation Patterns (PAP) enable these observers to be safely modified during execution without restarting the verification process.Kwiatkowska et al. (2011) introduced PRISM 4.0, which extended quantitative verification to priced probabilistic timed automata and supported techniques such as explicit-state model checking, statistical model checking, and optimal strategy generation.Brix et al. (2023) analyzed the first three editions of the International Verification of Neural Networks Competition (VNN-COMP), which evaluated tools on safety and robustness problems involving image classification, neural control, reinforcement learning, and autonomous systems.At the software engineering level, Chong et al. (2021) demonstrate how formal proofs can be integrated into continuous integration (CI), where verification artifacts are maintained with the codebase and checked as part of routine development workflows.Second, the evaluation focused on robustness against adversarial input perturbations and used Marabou and Planet as backend verification engines; the authors did not evaluate NARv with abstract-interpretation-based verification approaches.Henzinger et al. (2021) showed that verifying quantized neural networks with bit-vector specifications is PSPACE-hard, highlighting the computational difficulty of reasoning about rounding and fixed-point arithmetic.To improve scalability, they introduced three SMT-encoding optimizations: removing unreachable activation branches, minimizing bit-vector widths, and eliminating redundant multiplications.Future research should extend certification frameworks to cover additional trustworthiness dimensions, establish more widely accepted assessment metrics, and develop methods suited to increasingly complex systems, including foundation models and large language models.Gross (2023) examined the reproducibility of three studies and identified practical challenges involving software dependencies, hardware compatibility, missing implementations, and incomplete experimental documentation.Runtime Validation of Generative AI Outputs : Large language models (LLMs) can generate inconsistent or erroneous outputs, which raises reliability concerns in high-stakes applications.Overall, the findings demonstrate the potential of abstraction-refinement techniques to improve the scalability of formal neural network verification without sacrificing soundness or completeness under the approach's assumptions.Pulina and Tacchella (2012) introduced a Counter-Example Triggered Abstraction-Refinement (CETAR) approach that uses Quantifier-Free Linear Arithmetic (QF_LRA) to verify abstract network representations.Kaminwar et al. (2023) describe a structured approach that considers data, code, and model verification across development phases, emphasizing that evaluating predictive performance alone is insufficient to establish the reliability of an ML system.Isolated environments, such as Anaconda environments or Docker containers, can help manage software dependencies, while recording random seeds supports reproducibility when training involves randomness.POLAR provides polynomial arithmetic methods, whereas NNV supports multiple neural network architectures and learning-enabled control systems.PRISM is an open-source probabilistic model checker.

3.14 Tools, Frameworks, and Verification Workflows
Overview of Neural Network Verification Tools
Neural network verification tools analyze whether neural networks satisfy properties such as safety and robustness. They are important in safety-critical applications, including autonomous vehicles and cyber-physical systems. However, verification remains challenging because of network complexity, nonlinear behavior, and computational costs.
Different tools use different verification techniques. ReachNN focuses on reachability analysis for neural-network-controlled systems, while VeriSiG uses Taylor-model-based techniques to verify hybrid systems with neural network controllers. POLAR provides polynomial arithmetic methods, whereas NNV supports multiple neural network architectures and learning-enabled control systems. Tool selection depends on the network architecture, the property being verified, and the required balance between precision and computational efficiency.
SAT/SMT-Based Verification Frameworks
SAT/SMT-based frameworks encode neural network behavior and safety requirements as logical and mathematical constraints. Pulina and Tacchella (2012) introduced a Counter-Example Triggered Abstraction-Refinement (CETAR) approach that uses Quantifier-Free Linear Arithmetic (QF_LRA) to verify abstract network representations. Their experiments demonstrated the potential of SMT solvers for checking local and global safety properties, although scalability remained a challenge for complex networks.
Reachability Analysis Tools
Reachability analysis computes or approximates possible network outputs or system states from specified initial conditions, allowing safety and robustness properties to be evaluated.
NNV 2.0, introduced by Manzanas Lopez et al. (2023), supports feedforward, convolutional, recurrent, and semantic segmentation networks, as well as neural ODEs and neural network control systems. It uses representations such as star sets, zonotopes, and polyhedra, offering different trade-offs between precision and computational cost. In benchmark evaluations, NNV verified a larger proportion of properties in several cases compared with MATLAB’s Deep Learning Verification Toolbox, although performance varied across experiments.
Model Checking and Probabilistic Verification Software:
Probabilistic model checking analyzes systems involving uncertainty, nondeterminism, or timing by representing their behavior through formal probabilistic models. It can evaluate properties such as the probability of reaching an unsafe state and whether specified probability thresholds are satisfied.
PRISM is an open-source probabilistic model checker. Kwiatkowska et al. (2011) introduced PRISM 4.0, which extended quantitative verification to priced probabilistic timed automata and supported techniques such as explicit-state model checking, statistical model checking, and optimal strategy generation.
Storm is another open-source probabilistic model checker that supports reachability analysis, multi-objective verification, and parameter synthesis. In an evaluation of 96 benchmark instances, its fastest configuration solved 87 instances correctly (Hensel et al., 2022).
PRISM and Storm can complement neural network verification by analyzing system-level properties of AI-enabled systems under uncertainty. However, their results depend on the accuracy of the formal model and the properties supported by the chosen tool; they do not directly establish the correctness of an arbitrary neural network.
Specification Languages and Verification Benchmarks:
Specification languages describe the input constraints and output properties that neural networks must satisfy. VNN-LIB provides a standardized format for expressing neural network verification problems, helping different tools process common specifications.
Verification benchmarks are used to evaluate and compare tools using neural networks and specifications covering different verification tasks. Brix et al. (2023) analyzed the first three editions of the International Verification of Neural Networks Competition (VNN-COMP), which evaluated tools on safety and robustness problems involving image classification, neural control, reinforcement learning, and autonomous systems. Such benchmarks help assess verification performance and scalability. However, results depend on the selected networks, specifications, and experimental conditions, so they should be interpreted within the scope of each evaluation.
Integration with ML Development Pipelines:
Formal verification and structured verification practices can be incorporated into machine learning development pipelines to assess model reliability throughout the ML lifecycle. Kaminwar et al. (2023) describe a structured approach that considers data, code, and model verification across development phases, emphasizing that evaluating predictive performance alone is insufficient to establish the reliability of an ML system.
In practice, verification activities can be performed after model training and repeated when relevant components change. Developers can define formal properties, apply suitable verification tools, and use the results to guide model refinement. At the software engineering level, Chong et al. (2021) demonstrate how formal proofs can be integrated into continuous integration (CI), where verification artifacts are maintained with the codebase and checked as part of routine development workflows. Applying a similar approach to ML pipelines requires suitable support for the model format, specifications, and verification tool.
However, practical integration remains challenging because verification cost, tool compatibility, and model complexity can limit how frequently analyses are performed. Furthermore, an inconclusive verification result should be distinguished from a confirmed property violation. Consequently, an effective pipeline should report verification outcomes clearly and use them alongside other testing and evaluation activities.
Reproducibility and Verification Reporting :
Reproducibility is essential for validating experimental findings and comparing formal verification methods for neural networks. Gross (2023) examined the reproducibility of three studies and identified practical challenges involving software dependencies, hardware compatibility, missing implementations, and incomplete experimental documentation. The study highlights the importance of providing pretrained models, datasets, source code, dependency specifications, and clear instructions for running experiments.
Verification reports should also document the computational environment, hardware requirements, execution times, and any modifications needed to reproduce the experiments. Isolated environments, such as Anaconda environments or Docker containers, can help manage software dependencies, while recording random seeds supports reproducibility when training involves randomness. Furthermore, providing scripts for generating experimental results and comparison baselines facilitates independent evaluation. These practices help researchers reproduce reported findings, compare verification methods more reliably, and identify limitations that may affect experimental results.
Comparative Evaluation of Tools and Techniques :
Comparative evaluation is important for understanding the strengths and limitations of neural network verification tools. Performance should be assessed using multiple criteria, including verification time, memory consumption, the number of problems solved correctly, scalability, and support for different network architectures and verification properties. Standardized benchmarks, such as those used in the International Verification of Neural Networks Competition (VNN-COMP), facilitate more consistent comparisons by using common network and specification formats and controlled evaluation conditions
However, comparative studies show that verification performance depends on the characteristics of individual problem instances. König et al. (2024) evaluated several local robustness verification systems on a collection of 79 neural networks and found that no single algorithm consistently outperformed all others. Their results highlighted complementary strengths across verification methods, suggesting that the most suitable technique depends on the network, the property being verified, and the computational requirements. Therefore, tool selection should consider not only overall benchmark scores but also the intended application, supported model types, and acceptable verification cost.
3.15
Case Study 1: Verifying Robustness of a Neural Network Classifier
Neural network classifiers may produce incorrect predictions when their inputs undergo small perturbations. Formal robustness verification determines whether a specified property holds for all inputs within a defined region, rather than testing only a finite number of examples. Casadio et al. (2022) investigated how different robustness definitions affect neural network training and formal verification.
The experiments used Fashion-MNIST and a modified German Traffic Sign Recognition Benchmark (GTSRB), with images of (28 \times 28) and (48 \times 48) pixels, respectively. The authors compared baseline networks with models trained using standard robustness (SR), Lipschitz robustness (LR), and strong classification robustness (SCR). The Marabou verifier was used to evaluate the specified properties.
The results showed that Lipschitz robustness was difficult to verify: none of the evaluated networks satisfied this property for any test image under the experimental settings. However, networks trained using LR satisfied the weaker SR property for 100% of Fashion-MNIST images and 97% of modified GTSRB images. Moreover, the verifier proved robustness properties for only 0–1.5% of the accurate baseline network's test cases.
The study also found that data augmentation was generally less effective than adversarial and constraint-based training. Although data augmentation improved robustness when applied to a larger, 18-layer convolutional network, it remained less effective than the other constraint-driven approaches.
This case study demonstrates that high classification accuracy does not guarantee formal robustness. While testing and adversarial attacks can identify violations, formal verification aims to establish whether a property holds throughout the specified input region. However, verification success depends on the robustness definition, training method, and capabilities of the verification tool. Therefore, robustness requirements should be clearly defined and considered during both training and verification.
Formal Safety Verification of an Autonomous Vehicle Component:
Ivanov et al. (2020) investigated the safety of an F1/10 autonomous racing car controlled by a neural network trained using deep reinforcement learning. The controller used LiDAR measurements to generate steering commands. The authors modeled the vehicle dynamics and sensor observations and used Verisig to verify that the car remained at least 0.3 meters from the walls over a seven-second period.
The tool verified networks with up to 128 neurons in each of two hidden layers and approximately 40 LiDAR rays. However, configurations with 61 rays exceeded the ten-hour verification limit. Real-world experiments also showed that faulty LiDAR measurements could cause crashes, highlighting the gap between simulated and actual performance.
This study demonstrates that formal verification can support autonomous vehicle safety, but scalability and sensor uncertainty remain significant challenges.
Fairness Verification in an Automated Decision System :
Automated decision systems used in hiring, loan approval, and other critical tasks may produce discriminatory outcomes based on sensitive attributes such as race, sex, or age. Biswas and Rajan proposed Fairify, an SMT-based approach for verifying individual fairness in trained neural networks.
Fairify divides the input domain into smaller partitions and prunes inactive neurons to reduce verification complexity. Using the Z3 constraint solver, it determines whether fairness violations exist and provides either a fairness certification or a counterexample. The approach was evaluated on 25 real-world neural networks from four sources and showed improved verification scalability compared with baseline techniques.
This study demonstrates how formal verification can identify potential discrimination in automated decisions. However, verification remains challenging for large neural networks, and its conclusions depend on the specified fairness property.
Safety Constraints in a Reinforcement Learning Agent:
Fulton and Platzer (2018) proposed Justified Speculative Control (JSC), an approach that combines formal verification, runtime monitoring, and reinforcement learning to improve the safety of learned controllers. The authors evaluated their method using Q-learning in a simulated adaptive cruise control system, where a following car must avoid colliding with a leading car.
The system used the KeYmaera X theorem prover to verify the safety of the modeled controller and ModelPlex monitors to check whether observed behavior complied with the model. When the model remained accurate, the learning agent was restricted to verified safe actions. In simulations with an accurately modeled environment, JSC produced no unsafe states during training and learned effective policies more efficiently than standard Q-learning. Under model perturbations, JSC also resulted in relatively few crashes, while a modified version, JSCQ, performed better as perturbations increased.
The study demonstrates how formal verification and runtime monitoring can provide safety guarantees during reinforcement learning under specified modeling assumptions. However, the experiments used a simplified simulated environment, and the authors identify evaluation in more complex environments as future work.
Runtime Validation of Generative AI Outputs :
Large language models (LLMs) can generate inconsistent or erroneous outputs, which raises reliability concerns in high-stakes applications. Zhang et al. proposed RvLLM, a runtime verification framework that checks LLM outputs against domain-specific constraints. The framework uses the Expert Specification Language (ESL), which allows domain experts to define customized predicates in a lightweight and intuitive way.
The authors evaluated RvLLM on three tasks: detecting violations of Singapore’s Rapid Transit Systems Act, numerical comparison, and inequality solving. Experimental results showed that RvLLM effectively detected erroneous outputs across different LLMs while remaining lightweight and flexible.
This study demonstrates the potential of incorporating expert domain knowledge into runtime verification to improve the reliability of generative AI systems. However, the framework’s effectiveness depends on the domain-specific constraints provided, and runtime verification does not necessarily guarantee the correctness of outputs beyond the properties being checked.
Evaluation Metrics, Benchmark Datasets, and Experimental Design
Liu et al. (2024) evaluated their NARv approach using verification time, the number of successfully verified properties, and the sizes of abstract and refined neural networks. Their experiments focused on verifying neural network robustness against adversarial perturbations and compared NARv with the existing verification tools Marabou and Planet, as well as the CEGAR-NN approach.
The evaluation used three benchmark groups: 45 neural networks from the ACAS Xu collision-avoidance system, one MNIST classification network, and two CIFAR-10 networks. The authors tested multiple perturbation thresholds and imposed time limits of one hour for individual verification problems, extended to ten hours for the MNIST and CIFAR-10 networks.
The results showed that NARv reduced verification time by 13.4%–86.3% for Marabou across almost all evaluated tasks and by 8.3%–78.0% for Planet across all evaluated tasks. Compared with CEGAR-NN, NARv was 11.6–26.6 times faster on average. These findings demonstrate how verification time, solved-property counts, and network size can be used to assess the effectiveness and scalability of formal verification methods.

Discussion of Verification Results and Limitations :
The results of Liu et al. (2024) show that the NARv approach improves the efficiency of exact neural network verification by combining abstraction and refinement. Compared with the original Marabou and Planet verification engines, NARv reduced verification time by 13.4%–86.3% for Marabou on almost all evaluated tasks and by 8.3%–78.0% for Planet across all evaluated tasks. It was also 11.6–26.6 times faster than the CEGAR-NN approach on average. These results indicate that reducing network size while preserving soundness can improve verification performance, particularly for difficult verification problems.
However, the study has several limitations. First, NARv was designed for fully connected feedforward neural networks, and its applicability to recurrent neural networks remains an open problem. Second, the evaluation focused on robustness against adversarial input perturbations and used Marabou and Planet as backend verification engines; the authors did not evaluate NARv with abstract-interpretation-based verification approaches. Third, the approach may provide limited performance improvements for verification problems that are already easy to solve.
Overall, the findings demonstrate the potential of abstraction-refinement techniques to improve the scalability of formal neural network verification without sacrificing soundness or completeness under the approach's assumptions. Nevertheless, further research is needed to extend the method to additional network architectures and investigate its integration with other verification techniques.
3.16 Challenges and Future Research Directions
Scalability of Formal Verification Methods :
Scalability remains a major challenge in formal verification, particularly when verification tools must account for the exact numerical behavior of deployed neural networks. Henzinger et al. (2021) showed that verifying quantized neural networks with bit-vector specifications is PSPACE-hard, highlighting the computational difficulty of reasoning about rounding and fixed-point arithmetic. To improve scalability, they introduced three SMT-encoding optimizations: removing unreachable activation branches, minimizing bit-vector widths, and eliminating redundant multiplications. Experiments on MNIST and Fashion-MNIST robustness benchmarks demonstrated speedups of more than three orders of magnitude over the baseline approach. However, these results were obtained on specific quantized networks and benchmarks; scaling formal verification to larger and more diverse architectures remains an open challenge.
Verification of Large and Complex Neural Networks :
Verifying large and complex neural networks is challenging because the increasing number of neurons and connections makes formal verification computationally expensive. Liu et al. (2024) proposed NARv, a network abstraction-refinement approach that addresses this challenge by simplifying a neural network before verification. It uses two abstraction operations: Merge, which combines hidden neurons, and Freeze, which replaces selected neurons with constant values. These operations construct an over-approximation of the original network, preserving soundness. If verification identifies a spurious counterexample, NARv refines the abstract network using Split and Recover operations to restore precision while excluding the spurious result.
The authors evaluated NARv on ACAS Xu, MNIST, and CIFAR-10 benchmarks using Marabou and Planet as verification engines. Their results showed reductions in verification time of 13.4%–86.3% for Marabou on almost all evaluated tasks and 8.3%–78.0% for Planet across all evaluated tasks. NARv was also 11.6–26.6 times faster on average than the comparison approach, CEGAR-NN. However, the method was primarily evaluated on fully connected feedforward networks. Although convolutional networks can be transformed into this representation, exploiting their specific structure remains an area for improvement, while verification of recurrent neural networks remains an open challenge.
Uncertainty and Distribution Shifts :
Uncertainty and distribution shifts remain important challenges in the formal verification of AI systems. Deep neural networks may perform well on training data but fail when encountering inputs from distributions that differ from those observed during training. Amir et al. (2024) proposed a verification-driven approach to assess the generalization of neural networks to out-of-distribution (OOD) input domains. Their method independently trains multiple neural networks and uses formal verification to measure the disagreement between their outputs across a specified input domain. Networks with higher disagreement are iteratively removed, retaining models whose decision rules are more consistent across the domain.
The approach was evaluated on Cartpole, Mountain Car, Aurora for Internet congestion control, and arithmetic neural networks. The experimental results showed that the method successfully identified models that generalized well to the evaluated OOD domains, including scenarios not represented in the training data. However, agreement between neural networks is used as an indicator of potential generalization rather than a universal guarantee of correctness. Moreover, the conclusions depend on the specified input domain and the assumptions encoded in the verification queries. Future research should therefore investigate broader uncertainty models and more diverse distribution shifts to strengthen the reliability of formally verified AI systems.
Compositional and Modular Verification :
Compositional verification is a promising approach to reducing the computational cost of verifying large neural networks. Instead of verifying the entire network as a single model, it decomposes the network into smaller subnetworks that can be verified sequentially. Duong et al. (2025) proposed CoVeNN, a verifier-independent framework that uses assume-guarantee reasoning to establish the correctness of the complete network. In this framework, intermediate output bounds serve as guarantees for one subnetwork and assumptions for the next. CoVeNN also applies iterative refinement to improve the precision of these assumptions when initial approximations are insufficient to prove the desired property.
The authors evaluated CoVeNN with neural network verifiers such as αβ-CROWN and NeuralSAT. Their results demonstrated reduced memory consumption and improved verification scalability on large networks, including ResNet-based models. The framework could also verify properties of larger networks that exceeded the memory capacity of the underlying verifiers when used directly. However, CoVeNN may return an unknown result when its refinement budget is exhausted, meaning that the desired property has not been formally established. Its effectiveness also depends on the network decomposition, the precision of intermediate bounds, and the capabilities of the underlying verifier. Future research should focus on improving decomposition strategies and refinement methods to extend compositional verification to increasingly complex neural architectures.

Hybrid Symbolic-Neural Verification Techniques :
Hybrid symbolic-neural verification combines neural networks with symbolic reasoning to verify complex properties of AI systems. Xie et al. (2022) proposed a neuro-symbolic verification framework that addresses a limitation of traditional neural network verification methods, which mainly support properties expressed as logical constraints over network inputs and outputs. Their framework introduces the Neuro-Symbolic Assertion Language (NESAL), which allows neural networks to be incorporated directly into logical specifications. These additional networks, called specification networks, act as proxies for complex semantic properties that are difficult to express using mathematical constraints alone.
The authors implemented a prototype Neuro-Symbolic Verifier (NSV) based on the Marabou verification framework and evaluated it using neural networks trained on the MNIST handwritten-digit dataset and the German Traffic Sign Recognition Benchmark (GTSRB). The experiments considered properties involving classification correctness, prediction confidence for inputs associated with the data distribution, and functional agreement between neural networks. Across 2,200 verification tasks, the prototype demonstrated the feasibility of verifying these neuro-symbolic properties. The approach also produced more informative counterexamples for certain distribution-related properties than conventional verification, helping developers identify potential network defects.
However, the evaluation was intended to demonstrate the feasibility of the framework rather than establish its scalability to very large networks. The experiments used resized images to keep verification computationally manageable, and one MNIST verification task reached the specified timeout. Furthermore, the framework depends on the quality of its specification networks, since errors in these networks can affect the meaning of the properties being verified. Future research should therefore investigate more scalable verification algorithms, improve the reliability of specification networks, and evaluate the framework on larger networks and more complex real-world systems.
3.16.6 Continuous Verification of Adaptive AI Systems
Continuous verification is an important challenge for adaptive AI systems because their behavior, operating environments, or requirements may change during execution. Repeating verification from the beginning after every change can introduce delays and interruptions, reducing the system’s ability to respond reliably. Carwehl et al. (2023) proposed a runtime verification approach for self-adaptive systems that supports changing requirements while preserving previously obtained verification results. Their method uses Property Specification Patterns (PSP) to generate formal properties and observer automata, while Property Adaptation Patterns (PAP) enable these observers to be safely modified during execution without restarting the verification process.
The approach was evaluated using an Arduino-based Body Sensor Network and the Timescales benchmark. The experimental results showed that dynamic observer adaptation was more than five times faster than redeploying and restarting the observers. The runtime verifier also correctly classified all 180 traces in the benchmark experiments. However, the evaluation covered a limited set of system requirements and adaptation patterns, so the results may not generalize to all adaptive systems. Furthermore, changes to requirements still involved human decision-making. Future research should extend continuous verification to more complex AI systems and investigate how verification properties can be updated safely as models, environments, and operational requirements evolve.
Formal Guarantees for Foundation Models and AI Agents :
Providing formal guarantees for foundation models and AI agents is challenging because these systems generate context-dependent outputs and may interact with external tools and environments. A promising approach is to specify the agent’s expected behavior formally and enforce compliance during execution. Crouse et al. (2024) proposed a declarative framework for formally specifying the high-level behavior of large language model (LLM)-based agents. Their framework represents agent behavior as a finite-state machine and uses Linear Temporal Logic (LTL) to express constraints on the sequence of states that an agent is expected to follow.
The proposed framework employs a decoding monitor to detect deviations from the specified behavior and a correction mechanism to guide generation back toward a valid sequence. Importantly, the monitor can operate with models accessed through APIs, without requiring direct modification of the underlying model. The authors demonstrated the framework by implementing existing agent architectures, including ReAct, ReWOO, and Reflexion, and introduced a new Plan-Act-Summarize-Solve (PASS) agent. Their experiments evaluated these approaches on three question-answering and reasoning benchmarks: HotpotQA, GSM8K, and TriviaQA. Among the agent-based methods evaluated, PASS achieved the highest exact-match accuracy on HotpotQA and TriviaQA, while ReAct performed better on GSM8K. The results also showed that combining non-agent prompting approaches with agent-based methods could improve performance across the evaluated datasets.
Despite these contributions, formal guarantees must be interpreted according to the properties being verified. The framework constrains the sequence and structure of agent outputs according to a predefined specification; it does not establish that generated statements are factually correct, that external tools return trustworthy information, or that every action is safe. Its effectiveness also depends on the accuracy and completeness of the specification. Therefore, future research should combine formal behavioral constraints with mechanisms for verifying tool outputs, enforcing safety policies, and monitoring interactions with dynamic environments. Such approaches could provide stronger, explicitly scoped guarantees for foundation-model-based systems without treating conformance to a behavioral specification as proof of overall correctness or safety.
Standardization and Certification of Trustworthy AI:
Standardization and certification are essential for translating the principles of trustworthy artificial intelligence into practical, measurable, and auditable requirements. Although numerous international standards, regulatory frameworks, and ethical guidelines have been developed, determining how to demonstrate compliance with these requirements at the technical level remains a significant challenge. Frischknecht-Gruber et al. (2024) addressed this gap by presenting a practical certification scheme for AI-based systems (AIS), developed through collaboration between academic researchers and an AI certification body. Their approach connects regulatory requirements and technical standards with explicit assessment objectives, criteria, metrics, and means of compliance.
The proposed certification scheme was developed through an analysis of 38 relevant documents, including standards and guidelines from ISO/IEC, IEEE, and the European Union Aviation Safety Agency, as well as European regulatory requirements. The scheme organizes trustworthy AI assessment around several key aspects, including human oversight, transparency, reliability, safety, and cybersecurity. It defines objectives for different phases of the AI system lifecycle, from requirements engineering and data management to model development, testing, deployment, and operation. The authors also identified 95 technical methods for assessing properties related to transparency, explainability, reliability, robustness, safety, and security. These methods provide practical ways to evaluate specific objectives and support the demonstration of compliance with relevant requirements.
A central contribution of this work is the integration of certification activities with requirements management and Machine Learning Operations (MLOps). The authors implemented the certification scheme using Jira to organize and trace assessment objectives and their associated means of compliance. They also developed an automated MLOps pipeline incorporating model and data versioning, automated testing, model evaluation, and monitoring. Changes to model source code or input datasets can trigger training and evaluation workflows, helping developers and certifiers track compliance as AI systems evolve. This approach supports continuous assessment rather than treating certification as a single evaluation performed only before deployment.
The scheme and its technical assessment methods were tested in two real-world computer vision applications: medical skin-lesion classification and vehicle detection at construction sites. These use cases provided a basis for evaluating the proposed workflows in different application contexts. The authors reported that the integration of structured requirements management, technical evaluation methods, and automated MLOps workflows supports traceability, reproducibility, and the systematic assessment of trustworthy AI objectives. However, the scheme remains a developing framework, and its coverage is not yet comprehensive across all dimensions of trustworthiness. In the version described in the paper, human oversight, transparency, reliability, safety, and cybersecurity are addressed to varying degrees, while data governance, fairness, and data privacy are identified as areas requiring further development.
From the perspective of formal verification, the paper highlights the importance of connecting high-level certification requirements with technical methods capable of evaluating specific system properties. The authors explicitly identify formal verification as one approach for using logical and mathematical proofs to assess whether defined criteria are satisfied. Nevertheless, the certification scheme combines different types of evidence, including quantitative metrics, empirical testing, documentation, and process-based controls. Consequently, not every assessment result constitutes a formal proof, and certification should not be interpreted as a guarantee that an AI system is universally correct, secure, or free from harmful behavior. The strength of the evidence depends on the property being assessed, the method selected, and the conditions under which the evaluation is performed.
Future research should extend certification frameworks to cover additional trustworthiness dimensions, establish more widely accepted assessment metrics, and develop methods suited to increasingly complex systems, including foundation models and large language models. Combining formal verification with systematic testing, risk management, and continuous monitoring could strengthen the technical evidence supporting certification. Such integration would help ensure that certification remains meaningful as AI systems change throughout their operational lifecycles.