Con la aplicación generalizada de robots en aeroespacial, medicina, automatización y otros campos, la seguridad de su movimiento es esencial para el bienestar de los humanos y el logro de programas socialmente beneficiosos vitales. Los diseños convencionales de hardware y software de robots principalmente se basan en conocimientos empíricos y pruebas manuales para garantizar la seguridad, pero esto no cubre todas las posibles rutas de prueba y agrega riesgos. Alternativamente, las verificaciones formales, matemáticamente rigurosas, pueden proporcionar garantías predecibles y confiables de la seguridad del movimiento del robot.