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 interoperability in the neural network verification community. 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.

Contributions and suggestions to the standard are welcome! If interested, please open an Issue describing your proposal on the GitHub repo.

(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[0,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