The increasing complexity of safety-critical avionics systems challenges traditional assurance approaches based primarily on testing and simulation. Although Level-D flight simulators provide high-fidelity environments for training and system validation, their integration with formal methods remains limited. This paper presents a practical framework for runtime and offline formal verification of avionics system behavior using real-time and logged data from Level-D flight simulators, integrated with NASA’s open-source flight software framework F’ (F Prime). Specifically, the framework focuses on the verification of autopilot mode transitions and flight control response properties, derived from data obtained from Airbus A320 and Boeing 787–9 Level-D simulators. Simulator-specific signals are abstracted into formal behavioral models, and safety and liveness properties are specified using temporal logic with explicit timing constraints. These properties are evaluated by a dedicated F’; monitoring component capable of detecting violations during replayed execution traces and live simulation runs. Finally, the results demonstrate that formal runtime verification can be effectively applied to industrial grade simulation environments, enabling early detection of undesired behaviors that may not be exposed through conventional testing.
Reinforcement learning for safety-critical tasks requires policies that are both high-performing and verifiably safe, particularly throughout the learning process. While model-predictive shielding offers a path to formal safety, existing methods are often computationally intractable for the high-dimensional, nonlinear systems where deep RL excels. We introduce Sparkd, a scalable shielding framework that overcomes this limitation. Sparkd leverages Koopman Operator theory to learn a globally linear representation of the environment’s dynamics in a lifted feature space, enabling efficient formal safety analysis. We further introduce a slack-augmented shielding optimization that guarantees feasibility while enforcing strict safety on executed actions, making the framework robust to model uncertainty and long-horizon conservatism. Our experiments demonstrate that Sparkd significantly reduces safety violations compared to existing safe RL methods while maintaining strong task performance in complex control environments.
Formal methods are particularly useful to guarantee safety before deployment in safety-critical tasks. Ensuring absence of collision for vehicles such as airplanes, cars, or robots is one common application of formal verification. However, many methods for verifying collision avoidance model a vehicle as a moving point mass, though real vehicles have non-zero area. Our prior work proposed a novel algorithm (the active corner method) for verifying collision avoidance for polygonal objects moving in the plane, along with a Python implementation. That implementation was not verified or certified, relying instead on a pen-and-paper proof of correctness. In this work, we describe an extension of the active corner method to fully automatically generate machine-checkable proof certificates of correctness for specific instances within the Prototype Verification System (PVS). This work briefly discusses the original active corner method proof approach, presents a novel algebraic approach that generalizes to any convex polygon, details the certification process with examples in PVS, and provides a case study using the differential dynamic logic integration within PVS. Our implementation, certificate examples, and proof scripts are available on GitHub .
OpenMP is a popular parallelization framework that lets users transform sequential code into parallel code with a few simple annotations. Unfortunately, it is also easy to inadvertently introduce errors by adding OpenMP pragmas into otherwise correct programs, including both logic errors and race conditions. We present a formal semantics for C code with OpenMP directives, building on the C semantics of the CompCert verified compiler and its extension to concurrency. Our semantics captures subtle interactions between OpenMP directives and variable state that have been obscured by previous OpenMP semantics, and provides a basis for detecting undesired behaviors introduced by incorrect annotations: in particular, any successful execution is guaranteed to be free of data races.
Rust’s type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic checks under Miri, but lacks static verification. We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library. We analyze the campaign’s effectiveness, discuss the practical value of machine-checked proofs for a subset of undefined behaviors (e.g., out-of-bounds access, null and dangling pointer dereferences, and use of uninitialized memory), and frame the remaining obstacles as open challenges for the formal-methods community.
This paper investigates a class of anomalous program behaviors, in which a variable use is syntactically guarded by a predicate, but the protection may be bypassed along certain execution paths due to the evaluation of other conditions in the surrounding logic. Consequently, the variable may further be involved in computations without the intended safety check, potentially causing unexpected execution outcomes or unsafe program states. We demonstrate that such anomalies may remain undetected by traditional testing criteria, including MC/DC, as well as by commonly used static checks. We formally define the anomaly pattern and provide a specification suitable for efficient systematic static analysis, formal verification, and test generation.
Scenario-based validation is a widely used technique for assessing the correctness of executable formal specifications, yet its effectiveness strongly depends on the adequacy of the scenarios used. Coverage measures have been commonly adopted to evaluate scenario adequacy, but it remains unclear whether higher coverage correlates with improved fault detection, especially at the level of formal specifications. While this relationship has been extensively studied for source code, it has received little attention in the context of executable formal models. In this paper, we investigate the relationship between coverage and fault detection capability for scenario-based validation of Asmeta specifications. We extend the AsmetaV tool with an extensive set of coverage criteria that go beyond existing macro rule coverage. To assess the effectiveness of these coverage criteria, we introduce a set of mutation operators for Asmeta specifications and conduct a large-scale mutation-based experimental study, based on scenarios generated through model-checking-based, random, and evolutionary techniques. Our results show that higher coverage is generally correlated with increased fault detection capability, but macro rule coverage alone is insufficient to capture scenario effectiveness and more fine-grained coverage criteria provide stronger correlation with mutation scores and lead to improved fault detection.
Deep neural networks (DNNs) are widely used in real-world computer vision applications, yet they remain vulnerable to errors and adversarial attacks. Formal verification offers a systematic approach to identify and mitigate these vulnerabilities, enhancing model robustness and reliability. While most existing verification methods focus on image classification models, this work extends formal verification to the more complex domain of object detection models. We propose a formulation for verifying the robustness of such models and demonstrate how state-of-the-art verification tools, originally developed for classification, can be adapted for this purpose. Through a comprehensive evaluation, we highlight the ability of formal verification to uncover vulnerabilities in object detection models, and derive formal robustness guarantees, underscoring the potential and need to further extend verification efforts in this domain. This work lays the foundation for further research into formal verification of object detection models across a broader range of computer vision applications. Our source code is publicly available online.( https://github.com/AvrahamRaviv/FVOD_2025 )
We introduce a method for the automatic learning of probabilistic automata from continuous-valued logs of long-running cyber-physical systems. Our method supports learning from sparse logs where no ground truth exists and succeeds without the need for manual hyperparameter tuning. We propose improvements to the Timed IOalergia algorithm and integrate it with a learning pipeline to tune discretization hyperparameters through non-convex optimization of a novel metaheuristic we call revision score. We demonstrate the effectiveness of our method through experiments on real-world and simulated datasets.
The single-core equivalence (SCE) technology provides the robust partitioning of multicore processors needed for estimating worst-case executing times (WCETs) and for FAA certification, which requires that change or failure of lower-criticality software does not affect higher-criticality software. However, SCE only allows running an application in a single core, and therefore cannot deal with emerging large safety-critical applications that do not fit in a single core. In this paper we introduce the physically multicore, logically single-core (PMLS) technology that extends SCE to such large applications—where different tasks may share variables and therefore have critical sections—which cannot be executed in a single core. The idea is to use well-known single-core methods, such as the single-core priority ceiling protocol (PCP), for task synchronization. We study schedulability properties of PMLS, formalize PMLS executions in Maude, and use model checking to find a task allocation that makes the large application schedulable (if one exists).
The adoption of large language models (LLMs) in hardware design automation poses correctness risks for safety-critical applications. We systematically evaluate LLMs against Satisfiability Modulo Theories (SMT) solvers across three hardware synthesis tasks, revealing that LLMs achieve lower levels of functional correctness compared to SMT approaches in our benchmarks. Our findings reveal a crucial distinction: whilst SMT solvers can excel at direct synthesis and can exhaustively validate LLM outputs, their counterexample feedback fails to improve LLM performance. This demonstrates that effective validation does not translate to effective improvement guidance for LLMs, establishing formal methods as essential for direct synthesis and a need for better iterative refinement methods in reliable AI-assisted hardware design.
The Realizable, Responsive, Unobtrusive Unit (R2U2) is a stream-based runtime monitoring framework that verifies a system’s adherence to a set of formal system requirements with minimal resource overhead, allowing for real-time, online monitoring on resource-constrained systems. Yet, a persisting challenge for deploying runtime monitors is eliciting formal specifications that accurately capture system requirements commonly expressed in ambiguous natural language; therefore, we employ NASA’s Formal Requirements Elicitation Tool (FRET) to configure R2U2 monitors from structured natural language requirements. We extend FRET to formalize requirements in Mission-time Linear Temporal Logic (MLTL) - the native specification logic of R2U2, and we provide 157 MLTL rewrite rules that reduce each of FRET’s MLTL formalizations by an average of 15 operators, or 36.05% , decreasing the resources necessary to monitor these requirements with R2U2. We also introduce a novel SMT-based proof technique for automatically proving the correctness of these rewrite rules.
This work presents a hardware-in-the-loop technique that enables a formal model to be connected directly to an external system. Thus, one can run and validate the formal model in a controlled and realistic environment. We implement the technique inside ProB via a new JSON-RPC communication library, along with new debugging features. Furthermore, we demonstrate the technique on drones, for which we (1) create a formal B model of safe drone movements, (2) train and use a reinforcement learning agent as an action planner, and (3) employ the B model as a safety shield. In this context, we analyze the challenges posed by the gap between the formal model and the real world. This workflow was successfully employed in two iterations of a master-level course as individual student projects. Our hardware-in-the-loop technique enables interactive control of the external drone system through animation or autonomous control through simulation. For debugging purposes, one can employ the existing debugging and visualization features of the ProB toolchain. Further, we developed a novel feature that links model states and executed actions with a video recording. The feature is useful for postmortem inspection of failed validation runs (e.g., drone crashes).
Cognitive architectures such as Soar are widely used to model human decision making in human–machine systems, but they are typically evaluated via simulation and therefore provide limited guarantees that do not cover all possible system behaviors. In this paper, we present a translation framework that compiles cognitive models in Soar into discrete-time Markov chains for analysis using the PRISM probabilistic model checker. The translation maps bounded abstractions of Soar’s working-memory elements to finite-domain PRISM variables, production rules to guards, and decision-cycle phases to an explicit control-state automaton. We demonstrate the approach on an augmented-reality surveillance case study, in which the translated Soar task model is synchronized with probabilistic modules capturing the evolution of cognitive attacks such as cybersickness, and its task-performance effects. The resulting PRISM models support quantitative verification of properties that depend on cognitive task progression and stochastic human-state dynamics.
The next generation of distributed quantum processors combines single-location quantum computing and quantum networking techniques to enable large entangled qubit groups to be established across remote processors, and for quantum algorithms to be executed distributively. We present DisQ, as the first formal model of distributed quantum processors, and permit the analysis of distributed quantum programs in the new computation environment. The core of DisQ is a distributed quantum programming language that combines the concepts of the Chemical Abstract Machine (CHAM) and Markov Decision Processes (MDP) to provide clearly distinguishable quantum concurrent and distributed behaviors. We also develop a simulation relation, based on classical simulation infrastructure, to verify the equivalence of a quantum algorithm and its distributed versions, enabling the equivalence check of the distributed version of a sequential quantum program.
Modern cyber-physical systems rely on complicated sensing pipelines to produce sensor estimates, which inherently contain uncertainty and may exhibit transient and recurring abnormalities. It is important to ensure system safety under such unavoidable uncertainty. We present a framework for CPS safety assurance under sensor uncertainty based on two key notions. First, we introduce tolerance contracts on sensor estimates, which specify how much, how long, and how frequently sensing abnormalities are permitted. Second, we leverage quantitative safety, which measures how close a CPS is to violating its safety requirements. Together, these notions enable rigorous reasoning about CPS safety in the presence of sensing abnormalities. We formalize the syntax and semantics of tolerance contracts and develop sound reasoning techniques for contracted CPSs. In particular, we formalize tolerance contracts within differential dynamic logic (d ℒ ) and develop a special invariant-style technique dedicated for reasoning with recurring abnormalities. A water tank case study demonstrates how different contract designs can be used to ensure system safety despite sensor uncertainty.
Many techniques for the automated verification of distributed protocols have been developed over the past several years, but their performance is still unpredictable and their failure modes can be opaque for industrial scale verification tasks. Thus, in practice, large-scale verification efforts typically require some amount of human guidance. In this paper, we present inductive proof decomposition, a new methodology for interactive safety verification that provides a compositional, interactive approach to inductive invariant development. Our approach guides the human-aided development of inductive invariants via a novel structure, an inductive proof graph, which is built incrementally by a human verifier, working backwards from a target safety property. A user is guided by induction counterexamples that are localized to specific nodes of this graph, and nodes of this proof graph are further decomposed based on logical actions that appear in a protocol’s transition relation. Our decomposition also enables a localized variable slicing technique that hides irrelevant protocol state at each sub-component of an inductive proof, allowing a user to focus on fine-grained sub-problems rather than a large, monolithic inductive invariant. We present our technique and experience applying it to develop inductive safety proofs of several complex distributed protocols, including the Raft consensus protocol, which is beyond the capabilities of modern automated verification tools. We also demonstrate how the developed proof graphs provide additional insight into the structure of a protocol proof and its correctness.
Mixed flow-sensitive analyses allow balancing efficiency and precision, and provide a convenient description for thread-modular analyses where shared data is analyzed flow-insensitively. The accumulation of flow-insensitive invariants during a flow-sensitive analysis can be readily encapsulated in update rules. In this paper, we formalize a generic interface for update rules in Isabelle/HOL, and provide correctness proofs for several implementations of update rules with various widening and narrowing techniques. As hosting solver, we formalize TD _side , an extension of the generic top-down solver that utilizes update rules to solve mixed flow-sensitive analysis problems. We establish its partial correctness relative to the update rule interface and thus for all implementations of the interface. To avoid unnecessary and potentially harmful iterations, we propose an algorithmic improvement for TD _side . This allows us to verify the optimality of TD _side ’s result—given a precise update rule and that the analysis problem satisfies certain monotonicity assumptions.
Traditional equivalence checking classifies programs as equivalent or non-equivalent, providing insufficient information for tasks like patch impact analysis where it is expected the patched version of the program to be non-equivalent to the original program. When two program versions are non-equivalent, determining under what conditions they differ and what percentage of inputs are affected remains an open challenge. In this work, we introduce quantitative partial equivalence analysis, an approach for assessing software patches by quantifying behavioral differences between the original (vulnerable) code and the patched code. Using symbolic analysis, we identify input conditions under which patched and original programs exhibit identical or divergent behaviors. Our approach refines non-equivalence by measuring the extent of behavioral divergence across the input domain. For efficient quantitative analysis of numerical domains, we propose a range-based search heuristic that provides a sound lower bound on equivalence. We demonstrate our approach on 90 CVE patches from widely used open-source projects (Linux, Qemu, FFmpeg), as well as on a Juliet Test Suite-based dataset containing programs with CWEs. Our results show that quantitative partial equivalence analysis effectively characterizes and quantifies patch impact. Additionally, experiments on the EqBench benchmark reveal five C program pairs that are mislabeled as equivalent, and we identify the input conditions under which their behaviors diverge.
Cyber-physical systems (CPS) such as autonomous cars, aircraft, and robots are often also safety-critical; thus it is imperative that they operate as intended with a high degree of certainty. Formal verification has been employed to verify the software controlling these systems, but due to their complexity, is usually performed on an abstract model rather than the executable code. Synchronous programming languages extended with differential equations promise both rigorous modeling and sufficient expressiveness to implement executable controller code, and recent developments have introduced formal verification of strictly discrete-time programs. Extending these verification techniques to hybrid systems enables precise modeling of the environment for a wider variety of programs to be both verified and executed. We formalize the operational semantics of initial value problems and zero-crossing detection expressed in a synchronous programming language, extend its type system for verification thereof, and prove its soundness.
