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.
