SENTINEL: A Multi-Level Formal Framework for Safety Evaluation of Foundation Model-based Embodied Agents
News
- [2026] SENTINEL is accepted to NeurIPS 2026! 🎉
- [2026] We release ManiGuard, our follow-up work that extends specification-grounded safety evaluation and improvement to robotic manipulation with VLA policies.
Abstract
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) specifications that can precisely specify state invariants, temporal dependencies, and timing constraints. It employs a multi-level evaluation 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 checked 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 checked 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 formal evaluation across multiple levels, SENTINEL provides a rigorous foundation for systematically evaluating the safety of FM-based embodied agents in simulation-based physical environments. It can effectively expose potential safety violations in interpreting, planning, and executing the tasks, and drive meaningful safety improvements through verifiable counterexample feedback.
Semantic Level Safety
At the semantic level, we evaluate whether LLM-based agents can correctly translate natural-language safety requirements into LTL specifications, the foundation for downstream plan- and trajectory-level checking. Generated formulas are first checked for syntactic correctness and then for logical equivalence with the ground truth via Büchi-automata-based language containment. Larger models such as GPT, Claude, and Gemini substantially outperform small open-source models, suggesting that base model capability plays a crucial role in both syntactic robustness and semantic fidelity.
| Model | Gen Succ ↑ | Syntax Err ↓ | Nonequiv ↓ | Equiv ↑ |
|---|---|---|---|---|
| Closed-Source LLMs | ||||
| GPT-5.5 | 99.3 | 0.0 | 28.4 | 71.4 |
| Claude-Opus-4.7 | 99.8 | 0.0 | 23.4 | 76.4 |
| Claude-Sonnet-4 | 99.7 | 0.1 | 17.8 | 82.1 |
| Gemini-2.5-Flash | 99.7 | 2.0 | 32.1 | 66.0 |
| Open-Source LLMs | ||||
| DeepSeek-V3.1 | 93.3 | 0.0 | 15.6 | 84.5 |
| Qwen3-14B | 95.9 | 1.6 | 70.7 | 29.1 |
| Qwen3-8B | 0.0 | – | – | – |
| Mistral-7B-Instruct | 96.5 | 11.7 | 90.8 | 0.1 |
| Llama-3.1-8B | 67.1 | 17.3 | 84.3 | 1.2 |
Semantic-level safety evaluation results on VirtualHome tasks (LTL safety prompt format).
Plan Level Safety
Plan-level evaluation determines whether safety interpretations translate into safe planning. High-level plans generated by LLM-based agents on 91 long-horizon VirtualHome tasks are checked against the LTL constraints derived in the semantic stage (5 sampled plans per task). Models that achieve higher equivalence in semantic interpretation also maintain higher plan-level safety (Pearson r = 0.990): accurate semantic grounding of safety rules is a prerequisite for reliable plan-level safety, underscoring the importance of SENTINEL's progressive evaluation design.
| Model | Succ ↑ | Safe ↑ | Succ & Safe ↑ |
|---|---|---|---|
| Closed-Source LLMs | |||
| GPT-5.5 | 90.2 | 89.9 | 86.9 |
| Claude-Opus-4.7 | 88.2 | 91.9 | 87.7 |
| Claude-Sonnet-4 | 85.5 | 91.2 | 84.6 |
| Gemini-2.5-Flash | 87.1 | 86.5 | 76.3 |
| Open-Source LLMs | |||
| DeepSeek-V3.1 | 89.5 | 96.5 | 88.8 |
| Qwen3-14B | 34.2 | 38.2 | 34.1 |
| Qwen3-8B | 0.3 | 0.0 | 0.0 |
| Mistral-7B-Instruct | 13.0 | 3.9 | 0.9 |
| Llama-3.1-8B | 16.5 | 5.7 | 1.3 |
Plan-level safety evaluation results on VirtualHome tasks (LTL safety prompt format).
Prompt-format ablation: LTL vs. natural-language vs. no safety prompt (Appendix C.1)
Adding explicit safety guidance improves plan-level safety for nearly all models, and formal LTL prompts yield the most consistent gains, suggesting that structured, machine-checkable constraints are more effective than free-form safety advice.
| Model | LTL Safety Prompt | NL Safety Prompt | No Safety Prompt | ||||||
|---|---|---|---|---|---|---|---|---|---|
| Succ | Safe | Succ & Safe | Succ | Safe | Succ & Safe | Succ | Safe | Succ & Safe | |
| Closed-Source LLMs | |||||||||
| GPT-5 | 68.2 | 73.9 | 67.7 | 66.0 | 71.8 | 66.0 | 62.4 | 68.0 | 62.3 |
| Claude Sonnet 4 | 85.5 | 91.2 | 84.6 | 84.6 | 90.6 | 83.7 | 77.3 | 82.2 | 76.4 |
| Gemini 2.5 Flash | 87.1 | 86.5 | 76.3 | 84.3 | 84.3 | 73.6 | 83.4 | 76.5 | 72.6 |
| Open-Source LLMs | |||||||||
| DeepSeek V3.1 | 89.5 | 96.5 | 88.8 | 88.9 | 94.2 | 84.1 | 89.1 | 83.4 | 78.2 |
| Qwen3 14B | 34.2 | 38.2 | 34.1 | 37.1 | 40.9 | 37.1 | 32.2 | 36.7 | 32.2 |
| Qwen3 8B | 0.3 | 0.0 | 0.0 | 0.0 | 0.0 | 0.0 | 0.2 | 0.0 | 0.0 |
| Mistral 7B Instruct | 13.0 | 3.9 | 0.9 | 13.7 | 4.7 | 1.2 | 13.9 | 4.1 | 1.5 |
| Llama 3.1-8B | 16.5 | 5.7 | 1.3 | 17.3 | 5.8 | 1.3 | 17.2 | 5.9 | 1.0 |
Trajectory Level Safety
At the trajectory level, safety evaluation requires reasoning over the full embodied execution process, where the simulator, low-level controllers, and FM-generated action plans all interact. Many physical safety violations can only be detected at this level:
We move evaluation to AI2-THOR, whose simulator provides grounded physical dynamics and object interactions, and evaluate LLMs with strong upstream planning ability as well as four VLMs on a suite of 120 short-horizon and 91 long-horizon safety-critical scenarios adapted from ALFRED, sampling 5 execution trials per task. Sampled trajectories are merged into a computation tree and checked with CTL across all execution branches. VLM-based agents tend to achieve higher safety but lower task success than LLM-based agents, reflecting a safety–capability trade-off at execution time. All agents still exhibit low Success & Safety, and the substantial drop from plan-level results suggests that unsafe behaviors often stem from low-level action arguments and the lack of built-in safety guarantees in controllers.
| Model | Succ ↑ | Safe ↑ | Succ & Safe ↑ |
|---|---|---|---|
| LLMs | |||
| GPT-5.5 | 67.8 | 67.3 | 51.7 |
| Claude-Opus-4.7 | 60.2 | 55.0 | 41.2 |
| Claude-Sonnet-4 | 55.3 | 26.9 | 11.1 |
| Gemini-2.5-Flash | 58.0 | 30.7 | 15.2 |
| DeepSeek-V3.1 | 54.7 | 34.9 | 15.0 |
| VLMs | |||
| GPT-5 | 54.8 | 67.8 | 42.8 |
| Gemini-2.5-Flash | 51.5 | 55.1 | 28.8 |
| GLM-4.6V | 43.6 | 56.9 | 28.6 |
| Gemma-3-27B-it | 30.5 | 77.3 | 15.6 |
Trajectory-level safety evaluation results across LLMs and VLMs on the full AI2-THOR test suite.
Safety Improvement via Verifiable Feedback
Beyond static evaluation, SENTINEL's verifiable counterexamples can be fed back to the agent in a refinement loop (max. 3 iterations). With Claude-Opus-4.7 as the base agent (and as the judge for the baseline), both feedback signals yield comparable task-success gains (+11.3 vs. +12.3 pp), but SENTINEL roughly doubles LLM-as-Judge's improvement on every safety metric (+10.8 vs. +5.2 pp on Safe; +14.6 vs. +8.5 pp on Safe + Success).
Trajectory-level improvement over baseline under SENTINEL vs. LLM-as-Judge feedback.
LLM-as-Judge labels on ground-truth safe/unsafe trajectories.
Why does LLM-as-Judge help less? It labels 95% of truly safe trajectories correctly, but misses nearly 83% of truly unsafe trajectories, either labeling them as safe or misidentifying the unsafe part, so its feedback signal is essentially uncorrelated with actual hazards.
From Simulation to a Real Robot
We task a Franka tabletop manipulator with heating food in a microwave while a metal object is already inside. Prompted with the
same task and safety constraints, the FM agent (with and without SENTINEL feedback) produces a
Safe plan that removes the metal object before heating and an Unsafe plan that heats directly. Both plans are executed
in AI2-THOR and on the Franka with key states aligned: SENTINEL's Unsafe verdict in simulation corresponds
to the same constraint violation, G(ON(microwave) ∧ HasMetal(microwave)), being satisfied on the real configuration.
A non-microwave-safe metal object (sim: spoon; real: aluminum can) is pre-placed inside the microwave. Top: the LLM-as-Judge agent fails all 3 loops (red circles mark the unattended object). Bottom: the SENTINEL agent corrects at loop 2, removing the spoon before heating.
Efficient CTL-Based Verification
Merging sampled trajectories into a single computation tree amortizes repeated state checking. CTL verification is consistently faster than a per-trajectory LTL baseline, with speedups growing to ~20× at 100 trajectories, and remains efficient as the number of safety constraints grows from 10 to 100 (and even 500).
Evaluation duration of CTL vs. LTL and the speedup ratio.
CTL checker runtime under 10–100 constraints.
Follow-up Work: ManiGuard
ManiGuard carries SENTINEL's specification-grounded view of safety to foundation-model robotic manipulation. It pairs task-level LTLf specifications with 200 benchmark tasks (1,000 ID/OOD scenarios) in Isaac Sim / OmniGibson and on a physical Franka, runtime-checked by automaton monitors over physics-grounded predicates, and releases 8,000 monitor-verified, safety-annotated demonstrations for safety-aware fine-tuning of VLA policies.
BibTeX
@inproceedings{zhan2026sentinelmultilevelformalframework,
title={SENTINEL: A Multi-Level Formal Framework for Safety Evaluation of Foundation Model-based Embodied Agents},
author={Simon Sinong Zhan and Philip Wang and Justin Liu and Yiyan Peng and Yiqi Lyu and Zinan Wang and Qineng Wang and Zhian Ruan and Xiangyu Shi and Xinyu Cao and Frank Yang and Zhenyang Ni and Kangrui Wang and Ruohan Zhang and Huajie Shao and Manling Li and Qi Zhu},
booktitle={Advances in Neural Information Processing Systems (NeurIPS)},
year={2026},
url={https://arxiv.org/abs/2510.12985}
}