# Formal Safety Guarantees for Autonomous Vehicles using Barrier Certificates

arXiv: https://arxiv.org/abs/2601.09740 · HTML: https://mlsanity.com/paper/2601.09740/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 7 references that are in the map.
- First posted on arXiv 8 Jan 2026.

## Builds on (most cited first, 3 of 3)

- [Control of Mobile Robots Using Barrier Functions Under Temporal Logic Specifications](https://mlsanity.com/paper/1908.04903/) (2019)
- [Barrier Function-based Collaborative Control of Multiple Robots under Signal Temporal Logic Tasks](https://mlsanity.com/paper/2102.02609/) (2021)
- [Decentralized Control Barrier Functions for Coupled Multi-Agent Systems under Signal Temporal Logic Tasks](https://mlsanity.com/paper/2011.12775/) (2020)

## Abstract (arXiv)

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.