# A Formal Safety Net for Waypoint Following in Ground Robots

## TL;DR

This paper introduces a formally verified safety net for ground robots that guarantees safe waypoint following by modeling, proving properties, and synthesizing runtime monitors, ensuring safety even with untrusted controllers.

## Contribution

It presents a reusable, formally verified safety framework for 2D waypoint-following in ground robots, integrating modeling, proof, and runtime enforcement with machine code guarantees.

## Key findings

- Formal safety and liveness guarantees for waypoint-following
- Runtime monitor enforces model compliance at execution
- Experimental validation confirms practical applicability

## Abstract

We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for 2D waypoint-following of Dubins-type ground robots with tolerances and acceleration. We: i) Model a robot in differential dynamic logic (dL), and specify assumptions on the controller and robot kinematics, ii) Prove formal safety and liveness properties for waypoint-following with speed limits, iii) Synthesize a monitor, which is automatically proven to enforce model compliance at runtime, and iv) Our use of the VeriPhy toolchain makes these guarantees carry over down to the level of machine code with untrusted controllers, environments, and plans. The guarantees for the safety net apply to any robot as long as the waypoints are chosen safely and the physical assumptions in its model hold. Experiments show these assumptions hold in practice, with an inherent trade-off between compliance and performance.