PV3 DNNV: Deep Neural Network Verificationverifies if a given property holds for a given neural network according to a given verifier

Framework that standardizes input and output formats, includes a DSL for specifying deep neural network (DNN) properties and provides simplification and reduction operations to facilitate the application, development and comparison of DNN verifiers.

Application domain/field

Type of tool


Expected input


Expected output

sat if the property was falsified, unsat if the property was proven to hold, unknown if the verifier is incomplete and could not prove the property, or error if there was an error. If the result was sat, indicating that a violation of the property was found, then DNNV also returns a counterexample.


Supports the following verifiers: Reluplex, planet, MIPVerify.jl, Neurify, ERAN, PLNN, Marabou, nnenum, verinet


License: MIT
DNN Neural network


Related papers

DNNV: A Framework for Deep Neural Network Verification (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to: VNNLIB and SOCRATES

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.