Formal Safety Guarantees for Autonomous Vehicles using Barrier Certificates
Oumaima Barhoumi, Mohamed H Zaki, Sofiène Tahar
TL;DR
This paper tackles the challenge of providing formal safety guarantees for AI-enabled autonomous vehicles in mixed-traffic environments. It proposes a TTC-based Barrier Certificate framework (TTC-BC) whose safe/unsafe regions are defined by a boundary on time-to-collision, and it leverages the Z3 SMT solver to verify safety invariants and enable adaptive speed control. The approach is validated on real-world data from the HighD highway dataset, reporting up to a 40% reduction in unsafe events (TTC < 3 s) and, in some lanes, complete elimination of conflicts, while maintaining interpretability via the TTC threshold. By combining formal verification with data-driven validation, the method provides interpretable and provable safety guarantees that are scalable for real-world deployment.
Abstract
Modern AI technologies enable autonomous vehicles to perceive complex scenes, predict human behavior, and make real-time driving decisions. However, these data-driven components often operate as black boxes, lacking interpretability and rigorous safety guarantees. Autonomous vehicles operate in dynamic, mixed-traffic environments where interactions with human-driven vehicles introduce uncertainty and safety challenges. This work develops a formally verified safety framework for Connected and Autonomous Vehicles (CAVs) that integrates Barrier Certificates (BCs) with interpretable traffic conflict metrics, specifically Time-to-Collision (TTC) as a spatio-temporal safety metric. Safety conditions are verified using Satisfiability Modulo Theories (SMT) solvers, and an adaptive control mechanism ensures vehicles comply with these constraints in real time. Evaluation on real-world highway datasets shows a significant reduction in unsafe interactions, with up to 40\% fewer events where TTC falls below a 3 seconds threshold, and complete elimination of conflicts in some lanes. This approach provides both interpretable and provable safety guarantees, demonstrating a practical and scalable strategy for safe autonomous driving.