Formal Methods

  • Guardrails for Foundational Model Enabled Robots | Current Topics

    Foundation models let a robots accept missions in natural language, but they also let a wrong or malicious instruction reach the propellers. PEACE [1] is a planner–executor agent for robots in which a large language model emits a complete, typed mission plan in a single call, and an independent safety service validates every motion command before actuation. That service currently enforces two geometric constraints: an altitude band and a horizontal geofence. It cannot express, let alone enforce, the rules that matter in the real world: keep distance from people, do not hover in front of windows, maintain a minimum altitude over roads, respect regulatory limits. This project replaces the geometric check with a two-tier guardrail: a plan-level check that grounds natural-language safety rules into formal specifications and verifies the whole mission plan before dispatch, and an execution-level check that grounds the same rules into spatial keep-out sets around detected objects.

    Show more...