PL/FM/SE Seminar Series: Adharsh Kamath, "Agent-C: Runtime enforcement for LLM agents."

Abstract: LLM-based agents are increasingly deployed in safety-critical applications, yet current guardrail systems fail to prevent violations of temporal safety policies, requirements that govern the ordering and sequencing of agent actions. For instance, agents may access sensitive data before authenticating users or process refunds to unauthorized payment methods, violations that require reasoning about sequences of action rather than an individual action. Existing guardrails rely on imprecise natural language instructions or post-hoc monitoring, and provide no formal guarantees that agents will satisfy temporal constraints. We present Agent-C, a novel framework that provides run-time guarantees ensuring LLM agents adhere to formal temporal safety properties. Agent-C introduces a domain-specific language for expressing temporal properties (e.g., “authenticate before accessing data”), translates specifications to first-order logic, and uses SMT solving to detect non-compliant agent actions during token generation. When the LLM attempts to generate a non-compliant tool call, Agent-C leverages constrained generation techniques to ensure that every action generated by the LLM complies with the specification, and to generate a compliant alternative to a non-compliant agent action. We evaluate Agent-C across two real-world applications: retail customer service and airline ticket reservation system, and multiple language models (open and closed-source). Our results demonstrate that Agent-C achieves perfect safety (100% conformance, 0% harm) in both benign and adversarial scenarios, while improving task utility compared to state-of-the-art guardrails and unrestricted agents. On state-of-the-art closed-source models, Agent-C improves conformance (from 77.4% to 100% for Claude Sonnet 4.5 and 83.7% to 100% for GPT-5), while simultaneously increasing utility (from 71.8% to 75.2% and 66.1% to 70.6%, respectively), representing a new state-of-the-art frontier for reliable agentic reasoning. The code for the Agent-C framework can be found at this link: https://github.com/structuredllm/agent-c.

This talk covers a paper co-authored by Sishen Zhang, Calvin Xu, Shubham Ugare, Gagandeep Singh, and Sasa Misailovic.  

Bio: Adharsh Kamath is a Ph.D candidate in the Siebel School of Computing and Data Science at the University of Illinois Urbana-Champaign. Adharsh is advised by Prof. Sasa Misailovic and works on formal methods, agentic AI and software engineering; broadly, Mr. Kamath is interested in finding ways to ensure reliability of software systems (those comprised of AI agents and those generated using AI agents).