Verifying Vision-Based Autonomy with Abstract Rendering and Perception Contracts

Vision-based autonomous systems are increasingly deployed in critical applications, yet verifying them end-to-end remains a formidable challenge due to uncertainties in image formation and the complexity of downstream ML-based perception. While perception contracts have been proposed to address this issue by bounding the possible outputs of a perception module, their guarantees are typically probabilistic. In this work, we propose a novel approach that integrates perception contracts with abstract rendering---a technique that computes rigorous, interval-based over-approximations of all possible rendered images under camera and scene uncertainties---to enable formal verification of vision-based autonomous systems.