Formal Verification of Neural Network Safety Beyond Toy Examples: Three Distinct Gaps and a Specification-First Research Agenda

Abstract

Formal verification of neural networks has matured into a real research area. Tools such as alpha-beta-CROWN, ERAN, and Marabou now reliably verify L-infinity robustness properties of ReLU networks at the ResNet scale, with the annual VNNCOMP competition documenting steady year-over-year progress. The dominant framing of what remains undone — "scale verification to bigger models" — captures only one of three distinct gaps that separate current capability from useful guarantees on frontier AI systems. This paper makes three claims. First, the scale gap (verifiers handle networks with millions but not billions of parameters), the architecture gap (standard techniques handle ReLU well but degrade sharply on transformers with softmax, attention, and layer normalization), and the specification gap (we lack formal definitions of "safe LLM output" comparable to L-infinity robustness for image classifiers) are independent obstacles that need independent attention. Second, the specification gap is the most underweighted of the three and may be the binding constraint: even with verifiers that scaled to trillion-parameter models, we would not have formal specifications of harmlessness, honesty, or nondeception to verify against. Third, the most productive near-term frontier is not direct verification of LLM weights but verification of the systems that contain LLMs — LLM-as-policy verification, runtime monitors, agent-action guardrails. We propose a research agenda that reorients around the specification problem and the system-level frontier rather than continuing to pursue parameter-count scaling as the central goal.