Verifying AI Models Before They Reach the Edge
At the edge, mistakes are expensive. Once an AI model is optimized, compiled, and connected to real sensors, failures are harder to diagnose. Therefore, it is crucial that AI systems behave as intended, particularly in safety-critical and mission-critical applications.
In this interactive, hands-on workshop, you will learn how to apply AI verification techniques, with a focus on formal methods, to build confidence in neural network behavior before deployment. Using real examples from aerospace applications (ACAS Xu collision avoidance), participants progress from finding adversarial examples to formally verifying global stability across an entire operational design domain.
Learn to move beyond sampling-based testing and gain mathematical verification of neural networks correctness across the entire operational design domain, catching deployment failures that Monte-Carlo approaches miss and getting ahead of emerging safety certification standards.
Example: The ACAS Xu collision avoidance system compresses a 2GB lookup table into 45 neural networks, reducing memory by over 99%. But how do we know these networks behave correctly in all situations? On the left, Monte-Carlo-based sampling evaluates individual points but cannot guarantee coverage. On the right, formal verification mathematically validates the model across the entire input space.
| Monte-Carlo-based Sampling | Formal Verification (Adaptive Mesh) |
|---|---|
 |
 |
| Monte-Carlo-based sampling leaves gaps in coverage. Zooming in reveals regions where network output is uncertain. With higher-dimensional inputs, these gaps grow larger or require exponentially more simulations to cover the ODD. | Formal methods mathematically validate that the network output is correct for ALL possible inputs, without needing to execute tests. The adaptive mesh iteratively verifies the entire ODD, leaving no gaps. |
| # | Exercise | Description | Results |
|---|---|---|---|
| 1 | Getting Started | Generate adversarial examples that fool a digit classifier | HTML |
| 2 | Local Robustness | Formally prove an ACAS Xu network is robust to input perturbations | HTML |
| 3 | Global Stability | Verify stability across the full operational design domain | HTML |
- Open MATLAB® R2026a or later (or click the "Open in MATLAB Online" badge above)
- Run
startup.mto configure paths, verify toolboxes, and download the ACAS Xu dataset - Open
Part1_GettingStarted.mas a Live Script and run section by section
Each exercise is self-contained. Exercises export published HTML results to results/ when run to completion.
- MATLAB® R2026a or later
- Deep Learning Toolbox™
- AI Verification Library for Deep Learning Toolbox™ (Add-On)
- Parallel Computing Toolbox™ — GPU acceleration for faster verification
- MNIST Digit Classification Network — A small CNN trained on handwritten digits (0–9). Ships with Deep Learning Toolbox.
- ACAS Xu Neural Networks — 45 fully connected networks from the Airborne Collision Avoidance System for unmanned aircraft. Each network takes 5 inputs (geometry and velocities) and outputs one of 5 steering advisories. Downloaded automatically by
startup.m.
- Explore ACAS Xu Neural Networks
- Verify Local Robustness of ACAS Xu Neural Networks
- Verify Global Stability Using Adaptive Mesh
Copyright 2026 The MathWorks, Inc.