Neural Network Verification
NeuralSAT is a DPLL(T) framework for proving or disproving safety properties of deep neural networks. Upload an ONNX model and VNNLib specification to begin.
Try NeuralSAT instantly with these pre-loaded benchmarks.
Neural Network (ONNX)
Drag & drop or click to browse
Specification (VNNLib)
Drag & drop or click to browse
Select a quick start example below, or upload your own network and specification files to begin.
Verifying…
Parsed layers and dimensions from the uploaded ONNX file. Note: Layers with more than 10 nodes are capped visually to maintain readability.
Upload an ONNX model to view architecture.
Safety specification details parsed from the VNNLib file.
Upload a VNNLib spec to view bounds.
Upload a VNNLib spec to view safety conditions.
Waiting for log stream...
NeuralSAT is a high-performance system for proving the safety and correctness of deep neural networks. It combines formal logical reasoning with optimization techniques to guarantee that neural networks behave correctly under all possible inputs. The tool supports fully-connected, convolutional, and residual networks with multiple activation functions.
ONNX: The standard exchange format used to represent the trained neural network model.
VNNLib: The specification file defining the range of inputs and the safety properties you want to verify.
UNSAT (Safe): The safety property is proven to hold. No input combination can violate the specification.
SAT (Violated): The property is disproven. A specific counterexample input has been found.
Timeout / Unknown: The verification did not complete within the time limit or could not be determined.