VNN-LIB

Introduction

VNN-LIB is an open-source standard for automated solvers of satisfiability problems over neural networks. The goal of the standard is to foster greater robustness and interoperability in the neural network verification landscape. To this end, the standard defines:

A formal syntax for defining satisfiability queries.
A formal semantics for that syntax.
A command-line interface for solvers.

(vnnlib-version <2.0>)

; Network declaration
(declare-network f
    (declare-input  X float32 [2,2])
    (declare-output Y float32 [1])
)

; Input constraints
(assert (and (>= X[1,0] 0.0) (<= X[0,0] 1.0)))
(assert (and (>= X[0,1] 0.0) (<= X[0,1] 1.0)))
(assert (and (>= X[1,0] 0.0) (<= X[1,0] 1.0)))
(assert (and (>= X[1,1] 0.0) (<= X[1,1] 1.0)))

; Output constraints
(assert (or (<= Y[0] -3.0) (>= Y[0] 0.0)))

Latest News

December 15th 2025
VNN-LIB 2.0 released
December 15th 2025
VNNLIB-Python 1.0.0 released
December 15th 2025
VNNLIB-CPP 1.0.0 released
December 15th 2025
VNNLIB-Agda 1.0.0 released
November 11th 2022
VNN-LIB 1.0 released

Solvers

Solvers that are known to support VNN-LIB.

Name	VNN-LIB Version
Marabou	1.0
NNV	1.0
Pyrat	1.0

To add a solver to this list, please open a pull request.

Documents

Released versions of the VNN-LIB standard.

Document	Release date
VNN-LIB 2.0	December 15th 2025
VNN-LIB 1.0	November 11th 2022

Citing the standard:

Version 1.0 - FoMLAS 2023: S. Demarchi, D. Guidotti, L. Pulina and A. Tacchella, Supporting Standardization of Neural Networks Verification with VNN-LIB and CoCoNet

Libraries

The following official libraries are available for interacting with the VNN-LIB standard.

C++

Parser

A C++ library for parsing VNN-LIB query files.

Functionality includes the generation of an AST from a VNN-LIB query, and utilities to transform the AST into other formats.