Formal verification of neural networks: what's usable today

Formal verification of a neural network means asking a tool whether a stated input-output property holds for every input in a region, not just for a test set. The official pages below describe research and commercial tools that do that for some networks. They do not, in the sources we checked, turn those tools into an FAA or EASA means of compliance.

Status as of 14 October 2026: the Marabou README still calls Marabou a research product, still documents the ACAS Xu command, still names version 2.0, and still says We no longer provide Windows support. nnenum’s README still does not name who-it’s-for or on-prem/SaaS/air-gapped. NNV still lists aerospace among application domains. α,β-CROWN still stays out of the directory because the pages we fetched do not name aerospace or defense. NNDK is listed separately as safety-engineering (formal package plus runtime monitoring); its fortiss page still does not name DO-178C. CAISAR (CEA List, 6.0 June 2026) is listed separately as safety-engineering; its docs name ACAS Xu as an example and do not name DO-178C. PyRAT is listed separately as the CEA AISER verifier (VNN-COMP 2024 second place on its site; CAISAR news ranks it third at VNN-Comp 2026); official pages do not name DO-178C.

What the research tools say they do

Marabou is an SMT-based tool that can answer queries over networks. A typical query is a neural network and a property. The result is either a formal guarantee that the network satisfies the property, or a concrete input for which the property is violated (a counter-example). The official README’s worked command verifies an ACAS Xu network. The resources README says the acasxu folder contains the ACAS XU benchmarks from the Reluplex paper. The Marabou 2.0 tool paper says Marabou is available under the permissive modified BSD open-source license.

nnenum is a high-performance neural network verification tool for ReLU networks. The official example verifies an ACAS Xu ONNX model. The README says nnenum was the only tool to verify all the ACAS-Xu benchmarks in VNN-COMP 2020. The NFM paper evaluates optimizations on the 180 ACAS Xu benchmarks.

NNV is a MATLAB toolbox for neural network verification using sound set-based reachability analysis. Official application domains include aerospace. The ACAS Xu tutorial calls ACAS Xu the canonical benchmark for neural network verification and a family of 45 neural networks designed to advise unmanned aircraft on collision avoidance maneuvers. A result of 1 (SAFE) means the property holds for ALL inputs in the specified region and is a formal guarantee. The repository describes NNV as an open-source MATLAB toolbox; GitHub reports no license file, so this directory does not give it an OSI badge.

ERAN is an analyzer based on abstract interpretation for the complete and incomplete verification of MNIST, CIFAR10, and ACAS Xu based networks. A documented command will run DeepZ for analyzing property 9 of ACASXu benchmarks.

Listings: Marabou, nnenum, NNV, ERAN. NNDK includes a formal-verification package (static analysis / constraint solving) alongside metrics and runtime monitoring; it is not an ACAS Xu verifier on the pages we cite.

Commercial pages in the same neighborhood

MathWorks AI Verification provides tools for assessing and verifying properties of deep neural networks, including robustness verification and output bounds. The airborne worked example includes the development and verification activities required by DO-178C, ARP4754A, and prospective EASA and FAA guidelines. That sentence is an example description, not a certification claim. See the listing caveat.

Saimple uses abstract interpretations to assess robustness. The vendor page names ISO/IEC 24029 and EASA work; see Saimple. Catalog text for that ISO series — including that it is not an FAA or EASA means of compliance we have found — is on ISO/IEC 24029 neural-network robustness.

A tool we read and did not list

α,β-CROWN is a neural network verifier and the README calls it the winner of VNN-COMP 2021, 2022, 2023, 2024, 2025. The official pages we fetched do not name aerospace or defense, so it is not in the directory. The README does say it can provide provable robustness guarantees against adversarial attacks and verify other general properties of neural networks, such as Lyapunov stability in control.

What those pages make usable, and what they do not

What the official examples actually run is small, mostly ReLU, feed-forward networks and image classifiers, with ACAS Xu as the aviation benchmark. Marabou, nnenum, NNV and ERAN each ship ACAS Xu artifacts. That is a property check on a network of that scale, in the tool’s supported format (ONNX, NNet, VNNLIB, MATLAB). We found no official source that treats those ACAS Xu artifacts as certified airborne software.

We searched those official docs and papers for a sentence that says the tool is an FAA advisory circular, an EASA acceptable means of compliance, or a substitute for DO-178C / DO-330. We did not find one. See Does the FAA certify AI today? and Mapping an AI model to DO-178C / DO-330.

Analysis, not sourced fact: a program can treat these tools as evidence generators for a stated property (robustness in a box, an ACAS Xu advisory constraint) and still need a conventional assurance case for the system. That stacking is a reading of the documents, not a requirement we found.

Questions

Can these tools formally verify a large language model today?

No official page we cite shows an LLM verification example. The shipped examples are ACAS Xu-scale networks and image classifiers.

Does an ACAS Xu benchmark result mean an aircraft is certified?

No. The official pages call ACAS Xu a benchmark or an example. MathWorks describes a worked airborne example. None of the cited pages say a verifier output is a type certificate.