# SENTINEL: A Multi-Level Formal Framework for Safety Evaluation of Foundation Model-based Embodied Agents

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 14 of its 53 references that are in the map.
- First posted on arXiv 14 Oct 2025.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 14 of 14)

- [Measuring Massive Multitask Language Understanding](https://mlsanity.com/paper/2009.03300/) (2020)
- [R-Judge: Benchmarking Safety Risk Awareness for LLM Agents](https://mlsanity.com/paper/2401.10019/) (2024)
- [ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning](https://mlsanity.com/paper/2503.22738/) (2025)
- [SafeAgentBench: A Benchmark for Safe Task Planning of Embodied LLM Agents](https://mlsanity.com/paper/2412.13178/) (2024)
- [OneTwoVLA: A Unified Vision-Language-Action Model with Adaptive Reasoning](https://mlsanity.com/paper/2505.11917/) (2025)
- [PlanGenLLMs: A Modern Survey of LLM Planning Capabilities](https://mlsanity.com/paper/2502.11221/) (2025)
- [IS-Bench: Evaluating Interactive Safety of VLM-Driven Embodied Agents in Daily Household Tasks](https://mlsanity.com/paper/2506.16402/) (2025)
- [SafeWatch: An Efficient Safety-Policy Following Video Guardrail Model with Transparent Explanations](https://mlsanity.com/paper/2412.06878/) (2024)
- [Generating Robot Constitutions & Benchmarks for Semantic Safety](https://mlsanity.com/paper/2503.08663/) (2025)
- [HAZARD Challenge: Embodied Decision Making in Dynamically Changing Environments](https://mlsanity.com/paper/2401.12975/) (2024)
- [LaMMA-P: Generalizable Multi-Agent Long-Horizon Task Allocation and Planning with LM-Driven PDDL Planner](https://mlsanity.com/paper/2409.20560/) (2024)
- [EARBench: Towards Evaluating Physical Risk Awareness for Task Planning of Foundation Model-based Embodied AI Agents](https://mlsanity.com/paper/2408.04449/) (2024)
- [LabSafety Bench: Benchmarking LLMs on Safety Issues in Scientific Labs](https://mlsanity.com/paper/2410.14182/) (2024)
- [Defining and Evaluating Physical Safety for Large Language Models](https://mlsanity.com/paper/2411.02317/) (2024)

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

- [CreFlow: Corrective Reflow for Sparse-Reward Embodied Video Diffusion RL](https://mlsanity.com/paper/2605.14274/) (2026)
- [Security and Privacy in Large-Model-Driven Embodied Agents: Attacks, Defenses, and Future Directions](https://mlsanity.com/paper/2609.27847/) (2026)

## Abstract (arXiv)

We present SENTINEL, a framework for formally evaluating the physical safety of foundation model (FM)-based embodied agents. SENTINEL is the first to provide multi-level safety evaluation across semantic interpretation, plan generation, and physical execution within a unified formal framework. Unlike prior methods that rely on heuristic rules or subjective FM judgments, SENTINEL grounds practical safety requirements in formal temporal logic (TL) semantics that can precisely specify state invariants, temporal dependencies, and timing constraints. It employs a multi-level verification pipeline where (i) at the semantic level, intuitive natural language safety requirements are formalized into TL formulas and the agent's understanding of these requirements is probed for alignment with the TL formulas; (ii) at the plan level, high-level action plans and subgoals generated by the agent are verified against the TL formulas to detect unsafe plans before execution; and (iii) at the trajectory level, multiple execution trajectories are merged into a computation tree and efficiently verified against physically-detailed TL specifications for a final safety check. We apply SENTINEL in VirtualHome and AI2-THOR, and formally evaluate multiple FM-based embodied agents against diverse safety requirements. Our experiments show that by grounding physical safety in temporal logic and applying verification methods across multiple levels, SENTINEL provides a rigorous foundation for systematically evaluating the safety of FM-based embodied agents in simulation-based physical environments, and can effectively expose potential safety violations in interpreting, planning, and executing the tasks.