# A Summary of Formal Specification and Verification of Autonomous Robotic Systems

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Nov 2019.

## Built on by (most cited first, 4 of 4)

- [Auditing of AI: Legal, Ethical and Technical Approaches](https://mlsanity.com/paper/2407.06235/) (2024)
- [Monitoring of Perception Systems: Deterministic, Probabilistic, and Learning-based Fault Detection and Identification](https://mlsanity.com/paper/2205.10906/) (2022)
- [Address Behaviour Vulnerabilities in the Next Generation of Autonomous Robots](https://mlsanity.com/paper/2103.13268/) (2021)
- [Real-Time Model Checking for Closed-Loop Robot Reactive Planning](https://mlsanity.com/paper/2508.19186/) (2025)

## Abstract (arXiv)

Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions of Luckcuck 2019, which surveys the state-of-the-art in formal specification and verification for autonomous robotics.
