Neural network (NN) verifiers are increasingly used to certify safety properties such as robustness (i.e., small allowed perturbations to an input should not alter a model’s decision). Since verifiers aim to prove the absence of violations by considering all possible specified behaviors, the soundness of their implementations is therefore critical to guaranteeing correctness. Detecting unsoundness is particularly important and challenging, because a verifier typically spans multiple components, including specifications, neural networks, operator semantics, and constraint solving, where subtle implementation bugs can silently lead to \emph{false} certified results.

We present an approach for neural network robustness verifiers that detects and localizes soundness-relevant faults via two types of concrete–abstract consistency checks: (1) \textit{Counterexample-Based Refutation} (CBR), where a certification is supposed to be refuted if a concrete counterexample is found at runtime; and (2) \emph{Bounds-Based Localization} (BBL), which audits per-neuron containment (concrete activations must lie within abstract bounds as an invariant) to pinpoint incorrect implementations at particular NN layers or operators. To reduce representation drift, we use specification-embedded models that wrap the core NN with input and output specifications as two additional layers. We further develop an operator-aware NN generator that can produce diverse NN models spanning a wide range of layer types, parameters, and architectures, enabling systematic exposure and exercise of different operator behaviors.

We evaluate neural network verifiers on three abstract domains using six mutation operators. Across 450 soundness-violating instances, our framework detects 73% of injected soundness violations. CBR mainly exposes input-output-level soundness failures when a concrete counterexample is found during input sampling, while BBL catches internal bound-containment violations and localizes them to specific layers/operators, even when CBR becomes ineffective in high-dimensional inputs. These results indicate that combining coarse refutation (CBR) with fine-grained invariant checking (BBL) provides practical assurance for robustness verifiers, and operator-aware generation further boosts both coverage and discovery of unsoundness issues.