SafeTap: Trustworthy Neurosymbolic Language to Quadrupedal Locomotion via Shield Synthesis Modulo Bitvectors

Large language models (LLMs) are increasingly used to control embodied agents by mapping natural-language commands to high-level actions. While this paradigm enables flexible human-robot interaction, it also introduces significant safety risks, as LLM-generated commands are not guaranteed to respect physical, environmental, or mission-critical constraints. In this paper, we present an application of reactive synthesis modulo theories to the real-time guardrailing of an LLM-controlled quadruped robot, using the first-order theory of bitvectors as a symbolic abstraction of the robot's action space and environment.

Our system translates natural-language commands into discrete bitvector-encoded actions, which are then filtered by a formally synthesized guardrail (also called shield) that enforces safety and liveness properties expressed in Linear Temporal Logic modulo bitvector constraints. The shield operates online and corrects unsafe commands while preserving the intent of the human operator. We instantiate our framework in a realistic locomotion setting, inspired by recent work on language-driven robot control, and demonstrate that the robot maintains safety under adversarial and dynamic environmental conditions.

This work illustrates how theory-aware synthesis can serve as a practical foundation for trustworthy human--robot interaction, enabling the deployment of learning-based controllers in safety-critical settings with formal guarantees.