What NNV3 is, in builder terms

NNV3 is the latest version of the Neural Network Verification (NNV) tool, a MATLAB framework for formal verification of deep learning models and learning-enabled cyber-physical systems (CPS). 1

The core idea across NNV’s versions is set-based reachability: instead of checking one input at a time, you reason about *sets* of possible inputs and how a network maps entire sets forward through its layers. 1

Concretely, the tool has evolved in three stages:

  • NNV 1.0 – set-based reachability for:
  • Feed-forward neural networks (FFNNs),
  • Convolutional neural networks (CNNs),
  • Neural-network–controlled systems (NNCS). 1
  • NNV 2.0 – adds coverage for:
  • Recurrent neural networks (RNNs),
  • Spiking and similar structured networks (SSNNs),
  • Neural ordinary differential equations (neural ODEs). 1
  • NNV 3.0 (NNV3) – expands to:
  • New “Star-set family” members: ModelStar, VolumeStar, GraphStar,
  • A conformal-inference-based probabilistic reachability mode,
  • FairNNV for certifying counterfactual and individual fairness,
  • New domain benchmarks and unified documentation. 1

For someone building agentic systems, the relevant mental model is:

NNV3 sits *alongside* your training/evaluation stack and gives you ways to prove or statistically bound what your networks can and cannot do under classes of inputs, perturbations, or fairness constraints.

Everything runs in MATLAB; the paper describes it explicitly as a MATLAB framework. 1

How NNV’s set-based reachability works, structurally

The paper states that NNV is built on a set-based reachability foundation and that NNV3 introduces “new members of the Star-set family.” 1 While the abstract does not specify the exact data structure, the control flow is conceptually:

  1. Specify an input region

Instead of a single input vector (e.g., one image, one signal), you define a *continuous input region*—for example, a set of images within some perturbation bound or a range of sensor readings. FairNNV explicitly works over “continuous input regions.” 1

  1. Lift that region into a set representation

NNV uses a family of set representations referred to as Star sets. NNV3 extends this family with variants designed for specific use cases (weight perturbations, video/3D, graphs). 1

  1. Propagate sets through the network or system

The set-based reachability engine propagates these sets through:

  • FFNNs, CNNs, NNCS (NNV 1.0),
  • RNNs, SSNNs, neural ODEs (NNV 2.0),

now extended to NNV3’s new Star-set variants. 1

  1. Check properties on reachable sets

You encode a property (“the network never outputs a control that leaves a safe set,” “the classifier is invariant under some perturbation,” “outputs for individuals in a region differ by at most X”).

NNV then checks these against the set of reachable outputs. For fairness, FairNNV specifically targets “counterfactual and individual fairness properties over continuous input regions.” 1

  1. Choose deterministic vs probabilistic analysis

For some problems deterministic set-based reachability is “intractable.” NNV3 adds a probabilistic reachability mode based on conformal inference as a complement to sound (fully formal) analysis in those cases. 1

As a builder, you can think of NNV as providing multiple “modes” of analysis over the same underlying networks, depending on model class and tractability.

New Star-set members: what they are for and how to use them

NNV3 introduces ModelStar, VolumeStar, and GraphStar as “new members of the Star-set family.” Each is specialized for a particular type of uncertainty or input domain. 1

ModelStar: reasoning about weight perturbation

ModelStar is designed “for verifying networks under weight perturbation.” 1

Mechanically, this means the uncertainty set is not just over inputs, but over the parameters of the network:

  • You define a region of weight perturbations (for example, modeling quantization, compression, or bounded training drift).
  • ModelStar represents these perturbations as a set and plugs into the reachability machinery.
  • The verifier answers questions of the form: *for all weights within this region and for all inputs in a given input region, does the property hold?* (That general form is implied by “verifying networks under weight perturbation.” 1)

Where this matters for agentic systems:

  • Deployment changes (e.g., model compression, hardware-specific quantization) could be modeled as weight perturbations.
  • Online fine-tuning could be approximated as a neighborhood of weights around a base model.
  • ModelStar gives you a way to formally reason about “will my safety property survive small modifications to the network?” within the perturbation regime you specify.

Trade-off surface (as implied by the high-level description):

  • Larger weight-perturbation regions mean more conservative or intractable set propagation.
  • Narrow regions give tighter, more useful guarantees but cover fewer real-world changes.

VolumeStar: video and 3D volumetric inputs

VolumeStar is introduced “for video and 3D volumetric inputs.” 1

This is a direct extension of set-based reachability from 2D inputs (images) to spatiotemporal or 3D data:

  • For video, your input region is a *sequence* of frames with some allowed variation.
  • For volumetric data, your input region is a 3D grid or volume (e.g., a medical scan) with perturbations.

Operationally for builders:

  • If you are verifying perception in video-based systems (e.g., action recognition, video-based monitoring), VolumeStar gives you a way to pose input sets across both space and time.
  • For 3D domains like medical imaging, you can specify volumetric perturbations (e.g., noise, small geometric changes) and verify classifier or detector behavior across those.

NNV3 explicitly lists medical imaging and action recognition among its new benchmarks, which aligns with VolumeStar’s target domains. 1

GraphStar: graph neural networks

GraphStar is “for graph neural networks.” 1

While the abstract does not detail the set representation, the use case is clear: you can now bring graph-structured models into the same verification framework.

NNV3 includes new benchmarks for graph-based power-system models. 1 This suggests GraphStar is designed to handle:

  • Structured inputs where nodes/edges encode physical or logical infrastructure (e.g., power grids),
  • Properties around stability, safe operating regions, or classification on graphs.

For agentic stacks that operate over graphs (e.g., planners or controllers built on top of GNN estimators), GraphStar lets you pose “for all graph perturbations in this region (loads, topology tweaks, etc.), does the property hold?” using the same set-based paradigm.

Probabilistic reachability when verification is hard

Deterministic set-based verification can blow up in complexity. The authors state that:

“A conformal-inference-based probabilistic reachability mode complements sound analysis for problems where deterministic verification is intractable.” 1

Key ideas for builders:

  • Two regimes:
  • Sound (deterministic): traditional NNV-style reasoning, where if the tool says “property holds,” that is a formal guarantee under the specified model and input/weight regions.
  • Probabilistic: uses conformal inference to provide probabilistic reachability statements when the deterministic route is too expensive. 1
  • Control flow:
  • You attempt standard reachability.
  • If the problem is flagged as intractable (e.g., due to dimensionality or complexity of sets), you can switch to or augment with the probabilistic reachability mode.

From a system design perspective:

  • This gives you a degradation path: you don’t have to choose between “full proofs” and “no analysis.”
  • For some system components (e.g., less safety-critical perception), probabilistic guarantees might be acceptable as long as their limitations are explicitly tracked.

The abstract does not quantify coverage or error rates; it only states that the approach is based on conformal inference and is meant for intractable deterministic cases. 1

FairNNV: certifying fairness on continuous regions

NNV3 includes FairNNV, which:

“certifies counterfactual and individual fairness properties over continuous input regions.” 1

Two important aspects:

  • Counterfactual fairness (as referenced) typically concerns: *if we change a sensitive attribute while holding other relevant features fixed, does the outcome stay within some constraint?*
  • Individual fairness concerns: *similar individuals should receive similar outcomes.*

The paper does not define these formally, but it is explicit that FairNNV:

  • Works over continuous input regions, not pointwise tests,
  • Provides certification of these fairness properties. 1

For builders:

  • You can treat FairNNV as an additional verification layer over models in domains like malware detection, medical imaging, and others that NNV3 benchmarks, as long as the fairness notion can be expressed in terms of relationships between inputs in a continuous region. 1
  • Integrating FairNNV in a CI pipeline would mean: if a model update breaks a certified fairness property in a specified region, you get a hard failure instead of discovering it via ad-hoc testing later.

Design trade-offs (implied by the need for continuous-region reasoning):

  • The more expansive your continuous region and the more complex your fairness predicate, the more expensive the certification.
  • Narrower or more structured regions can keep analysis tractable, but they may miss important real-world unfairness modes.

Where NNV3 fits in an AI + CPS stack

The abstract positions NNV3 as a tool for “deep learning models and learning-enabled cyber-physical systems.” 1

A reasonable integration story, consistent with the paper’s scope:

  • Modeling & training

You train your models—FFNNs, CNNs, RNNs, SSNNs, neural ODEs, GNNs, etc.—using your usual frameworks, but export them in a form consumable by MATLAB/NNV3. 1

  • System-level CPS modeling

For NNCS and learning-enabled CPS, you have plant and controller dynamics modeled; NNV’s earlier versions already support NNCS, and NNV3 builds on that foundation. 1

  • Verification stage

You plug your models into NNV3:

  • For standard perception/control safety, you use the existing reachability stack (FFNN/CNN/RNN/etc.).
  • For video/3D domains, you use VolumeStar.
  • For GNN-based components, you use GraphStar.
  • If deployment modifications are in scope, you use ModelStar to account for weight perturbations.
  • For fairness, you run FairNNV over specified continuous input regions.
  • When full reachability is too expensive, you fall back to the conformal-inference-based probabilistic mode. 1
  • Benchmarks as templates

NNV3 provides new benchmarks in:

  • Malware detection,
  • Graph-based power-system models,
  • Medical imaging,
  • Variable-length time series data,
  • Action recognition. 1

For a builder, these serve as worked examples: you can align your application with the closest benchmark domain and modify the pipeline rather than starting from scratch.

  • Documentation & onboarding

NNV3 “incorporates tutorials and developer guides through a unified documentation site.” 1 That suggests you can expect concrete walkthroughs for the different model classes and verification modes, which is important if your team is new to formal verification.

Why this matters now for people shipping agents

From the abstract alone, several implications for current agentic systems are clear:

  • Coverage of more realistic models and inputs

The evolution from NNV 1.0 (FFNNs, CNNs, NNCS) to NNV 2.0 (RNNs, SSNNs, neural ODEs) and now to NNV3 (with ModelStar, VolumeStar, GraphStar) parallels the shift from simple controllers to richer, temporal and structured models used in CPS and decision-making systems. 1

If your agents rely on RNNs, neural ODE-based dynamics models, GNNs, or multi-frame inputs, NNV3 is explicitly designed to bring those under a unified verification umbrella.

  • Bridging the gap between “hard proofs” and “no guarantees”

The addition of probabilistic reachability using conformal inference acknowledges that not all practically interesting systems are tractable for full deterministic verification, but you still want structured statistical guarantees instead of ad-hoc testing. 1

  • Fairness as a first-class verification target

FairNNV’s support for “counterfactual and individual fairness properties over continuous input regions” makes fairness constraints something you can try to formally certify, not just evaluate empirically. 1 For agents acting on humans (e.g., malware filters, medical decision support, or other classification-heavy pipelines), this is directly relevant.

  • Benchmark-driven development

Benchmarks for malware detection, graph-based power-system models, medical imaging, variable-length time series, and action recognition give concrete, varied examples that map to significant real-world use cases. 1 That matters because deploying formal verification typically fails not on theory but on lack of domain-adapted examples and tooling.

What to watch next

Based on the abstract’s claims, several questions will determine how NNV3 lands in real-world stacks:

  • Scalability of Star-set variants

ModelStar, VolumeStar, and GraphStar extend coverage, but the practical size of networks and perturbation regions they can handle is not specified. The usefulness for large-scale, production models hinges on this. 1

  • Effectiveness of probabilistic reachability

The conformal-inference-based mode provides a path around intractability, but the abstract does not state what kinds of guarantees (e.g., coverage levels) are attained in practice or how sensitive they are to distributional assumptions. 1

  • FairNNV’s expressivity vs. tractability trade-off

How expressive can your fairness properties be while still allowing certification over continuous regions? The abstract confirms FairNNV supports counterfactual and individual fairness properties, but does not quantify complexity limits. 1

  • Integration with non-MATLAB stacks

The tool is MATLAB-based; the abstract does not discuss interoperability with other ecosystems. Builders will need to see how smooth the export/import path is from their preferred frameworks into NNV3’s world. 1

What is not documented

From the abstract alone, the following are not established:

  • Concrete algorithms or data structures for Star sets, ModelStar, VolumeStar, or GraphStar beyond being set-based representations.
  • Specific performance numbers, scalability limits, or complexity bounds for any verification mode.
  • The exact mathematical form of the conformal-inference-based probabilistic reachability guarantees.
  • Implementation details of FairNNV (e.g., how fairness constraints are encoded or solved).
  • Any integration APIs, model format requirements, or interoperability details with non-MATLAB tools.
  • Detailed descriptions of the new benchmarks’ architectures, dataset sizes, or performance metrics.