← Return to Article Details Verifiable ROS2 Navigation Execution with Runtime Contracts under Dynamic Obstacle Uncertainty