The International Standard for the Verification of Neural Networks

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:

  1. A formal syntax for defining satisfiability queries.
  2. A formal semantics for that syntax.
  3. 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 2.0 - VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification A. Roy, A. Antony, A. Gimelli, and M.L. Daggitt, CAV 2026:
  • Version 1.0 - Supporting Standardization of Neural Networks Verification with VNN-LIB and CoCoNet S. Demarchi, D. Guidotti, L. Pulina and A. Tacchella, FoMLAS 2023

    • Libraries

    The following official libraries are available for interacting with the VNN-LIB standard in a variety of languages.

    C++

    Parser Type-checker

    Python

    Parser Type-checker

    Julia

    Parser Type-checker

    OCaml

    Parser

    Agda

    Parser Type-checker Semantics

    We welcome PRs to these libraries and ports to further languages!

    Related

    Projects that are referenced to in both historically and currently in the development of the VNN-LIB standard.

    VNN-COMP

    Competiton

    The annual neural network verification competition.

    ONNX

    Network models

    The standard format for representing machine learning models that VNN-LIB relies on.

    Benchmarks

    Benchmarks version 1.0

    Our benchmarks repository from current research case studies.

    Team


    Current Members

    Matthew Daggitt

    Matthew Daggitt

    Lecturer | University of Western Australia

    Allen Anthony

    Allen Anthony

    Post-Grad | University of Western Australia

    Ann Roy

    Ann Roy

    Post-Grad | University of Western Australia

    Andrea Gimelli

    Andrea Gimelli

    PhD Student | UniGE

    Armando Tacchella

    Armando
    Tacchella

    Full Professor | UniGE

    Past Members

    Stefano Demarchi

    Stefano Demarchi

    Post-Doc Researcher | UniGE

    Luca Pulina

    Luca Pulina

    Full Professor | UniSS

    Dario Guidotti

    Dario Guidotti

    Post-Doc Researcher | UniSS