Dependable AI: Critical Software Contributions Accepted at SAIV 2026 and FLoC 2026
Critical Software contributes to dependable AI with two accepted papers at SAIV and FLoC 2026, advancing formal methods for safety-critical machine learning.
Critical Software is proud to announce that two of our research papers, developed within the SONNX (Safe ONNX) working group, have been accepted for publication at SAIV 2026 and OVERLAY 2026, part of FLoC 2026 (Federated Logic Conference).
These contributions mark an important step toward enabling dependable and certifiable Artificial Intelligence (AI) in safety-critical industries such as aerospace, defense, and transportation.
SONNX (Safe ONNX) is a collaborative working group within the ONNX community focused on enabling the safe use of machine learning in safety-critical systems. Bringing together academic and industry partners, including Critical Software, Airbus, Thales, ONERA, CEA, IRT, and the University of Minho, the initiative aims to address key gaps in current ML frameworks, particularly around formal guarantees, traceability, and certification readiness.
The Challenge: AI in Safety-Critical Systems
While AI and Machine Learning (ML) are rapidly transforming industries, their adoption in safety-critical environments has remained limited. One of the key barriers is the lack of:
Formal guarantees about system behavior
Precise and unambiguous specifications
Traceability between models and implementations
Compliance with strict certification standards
Without these assurances, deploying AI in contexts where safety is paramount is not feasible.
Our Approach: Formal Methods for Machine Learning
Through our work in the SONNX working group, we are helping define a “safe profile” for ONNX, a widely used ML interoperability framework.
Our research applies formal methods (mathematically rigorous technique) to address these challenges by:
Eliminating ambiguity in model specifications
Defining precise formal semantics for ML operators and computational graphs
Enabling machine-checked verification of model properties
Supporting certification processes through traceable and verifiable artifacts
Two Complementary Contributions
SAIV 2026: Formal Specification and Verification of ML Operators
Our first paper introduces a structured workflow for specifying ML operators, combining:
Textual, mathematical, and example-based descriptions
A two-level formal specification:
High-level, capturing the mathematical semantics
Low-level, capturing implementation details
We prove that the low-level implementation correctly refines the high-level specification, ensuring that extracted code (e.g., in C) faithfully preserves the intended behavior.
Additionally, we demonstrate how to formally verify key properties of neural networks, such as robustness.
OVERLAY / FLoC 2026: Formalization of ONNX Computational Graphs
The second paper extends this approach to computational graphs, particularly ONNX graphs, where we define:
A formal, non-deterministic execution semantics (high-level)
A concrete implementation proven to be deterministic and semantically correct (low-level)
We also introduce methodologies to verify execution properties, such as inductive invariants, and address practical challenges in formal verification tooling.
From Theory to Practice
A key outcome of this work is a formally verified reference implementation of operators and graphs. This can serve as a trusted oracle against which optimized implementations can be tested.
More broadly, our work bridges the gap between formal methods and applied AI, bringing mathematical rigor from theory into real-world engineering practice.
Why This Matters
In safety-critical industries, certification is not optional — it is a requirement. However, certification depends fundamentally on formal guarantees. Our work contributes to:
Improving the certifiability of ML models
Increasing confidence in the dependability of AI-based systems
Supporting compliance with emerging industry standards
Without rigorous formal semantics, there can be no verification, no certification, and no assurance that implementations preserve model properties.
Looking Ahead
The integration of AI into safety-critical systems is no longer a question of if, but of how — and rigorous foundations like these are what will make it possible.
This work represents a step in that direction, providing both the theoretical framework and practical methodology needed to build dependable AI systems.
If you would like to learn more about this work or discuss its implications for safety-critical AI systems, reach out to our AI expert engineer, João Galego.