Harmonizing Parameterized Verification and Invariant Synthesis for Safety Envelopes in Black‐Box Autonomy
Lu Yu, Zhoubing Xiong, Helin Huang, Bing He, Jinjun Kuang · Concurrency and Computation Practice and Experience · 2025
ABSTRACT Assuring the safety of autonomous agents in critical applications presents a significant challenge, particularly when these agents use opaque “black‐box” logic like Large Language Models (LLMs) and are deployed across a parameterized family of system configurations. Traditional formal methods are insufficient for this task, struggling with both the combinatorial complexity of parameters and the unobservable nature of the agent's decision‐making core. This work circumvents the intractable task of direct internal analysis. Instead, we propose the synthesis and runtime enforcement of a computational safety envelope—a set of verifiable constraints derived from high‐level specifications. The central challenge is to synthesize an envelope that is provably sound and universally valid across an entire family of systems. To achieve this, our framework harmonizes two theoretical cornerstones: Parameterized verification, which lifts the safety proof from numerous concrete instances to a single, symbolic proof using Parameterized Transition Systems (PTS), and invariant‐driven synthesis, which translates abstract specifications into simple, monitorable state constraints. We establish the theoretical rigor of our approach with two key theorems: The Soundness of Parameterized Safety Verification , which guarantees that a single verification effort is sufficient for the entire system family, and the Runtime Safety Guarantee of the Safety Envelope , which formally proves that any action permitted by the envelope is inherently safe, regardless of the agent's internal computations. We validated this framework on a resource scheduling testbed, where an LLM agent's behavior was probed with deceptive “trap tasks.” Our synthesized envelope demonstrated statistically robust effectiveness, successfully preempting a significant majority of hazardous actions and confirming that system safety is a direct function of key operating parameters. In essence, this research advocates a paradigm shift from the intractable verification of an unknowable interior to the rigorous construction of a provably correct exterior.