Verca: Verifying Robustness of Constrained-Latent Autoencoders

1. Usage - Extract data using bash tar -xf verca.tar.xz - See "verca/core/README.md" for more information 2. Abstract Autoencoders, a type of neural network that learns to compress and reconstruct data, are increasingly used in safety-critical cyber-physical systems, such as semantic communication pipelines and robotic controllers. However, these systems open up new attack surfaces: adversaries can inject bounded, stealthy noise that bypasses detectors while causing unsafe behavior in downstream applications. Existing DNN verifiers cannot handle this setting: they can propagate bounds through layers in networks but offer no mechanism to enforce nonlinear constraints at intermediate layers, producing either timeouts or invalid counterexamples. We present Verca, a verification framework for autoencoder-based neural networks that provides sound robustness guarantees against adversarial latent-space attacks. Verca employs a two-phase approach: (1) formulating adversarial noise generation as a Mixed Integer Program (MIP) to compute sound over-approximated bounds on latent-space perturbations, and (2) injecting these bounds into branch-and-bound verification to provide end-to-end guarantees across the encoder, decoder, and downstream task model. Verca also introduces a constrained adversarial attack that extends PGD with explicit constraints enforcement, ensuring every reported counterexample is feasible by a practical attacker. Evaluated on 1500 verification properties constructed from two datasets, e.g., FashionMNIST and CIFAR10, Verca solves 87% of instances, outperforming state-of-the-art verifiers 𝛼𝛽-Crown (66%) and NeuralSAT (67%), while producing zero invalid counterexamples against 396 spurious violations reported by each baseline. Verca also finds 514 valid counterexamples, more than twice the 236 found by the baselines, and reduces branch-and-bound search by up to 1437 branches or 54 iterations on verification problems.