Abstract Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries like finance and healthcare that operate under strict policies. To address this limitation, we launched Automated Reasoning checks (ARc) : a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies. ARc performs multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that ARc exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text. ARc is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.

This paper introduces Alpacas, a domain-specific language and algorithms aimed at architecture modeling and safety assessment for critical systems. It allows to study the effects of random and systematic faults on complex critical systems and their reliability. The underlying semantic framework of the language is Stochastic Guarded Transition Systems, for which Alpacas provides a feature-rich declarative modeling language and algorithms for symbolic analysis and Monte-Carlo simulation, allowing to compute safety indicators such as minimal cutsets and reliability. Built as a domain-specific language deeply embedded in Scala 3, Alpacas offers generic modeling capabilities and type-safety unparalleled in other existing safety assessment frameworks. This improved expressive power allows to address complex system modeling tasks, such as formalizing the architectural design space of a critical function, and exploring it to identify the most reliable variant. The features and algorithms of Alpacas are illustrated on a case study of a thrust allocation and power dispatch system for an electric vertical takeoff and landing aircraft.

In the context of developing safe air transportation, our work is focused on understanding how Reinforcement Learning methods can improve the state of the art in traditional control, in nominal as well as non-nominal cases. The end goal is to train provably safe controllers, by improving both training and verification methods. In this paper, we explore this path for controlling the attitude of a quadcopter: we discuss theoretical as well as practical aspects of training neural nets for controlling a crazyflie 2.0 drone. In particular we describe thoroughly the choices in training algorithms, neural net architecture, hyperparameters, observation space etc. We also discuss the robustness of the obtained controllers, both to partial loss of power for one rotor and to wind gusts. Finally, we measure the performance of the approach by using a robust form of a signal temporal logic to quantitatively evaluate the vehicle's behavior.

In previous work, we defined a component oriented framework dedicated to the specification of embedded systems in the aeronautics domain. A component is defined as a formal entity with three internal layers together with a collection of models defined in domain-oriented views. A categorical framework has been proposed to provide a unified representation of the component calculus as well as the various formal models used for the analysis of the system. In this paper, we present an implementation of this categorical framework using the EXPRESS data modelling language. EXPRESS is used to give an operational representation of the formalization, which is quite different from classical implementations of category theory based approaches.

This paper presents a component oriented framework dedicated to the specification of embedded systems in the aeronautics domain. A component is an entity with three internal layers (hardware, operating functions and applicative functions) together with a collection of models in different domain-oriented views. A composition operation allows the expression of composition scenarios, yielding a component calculus for representing composite systems. An institutional framework supports this component calculus, allowing the expression of coherence criteria between heterogeneous views. This framework can be seen as a formal documentation of a system development and analysis, supporting heterogeneous modeling and compositional verification. The approach is illustrated on a non trivial case study.