This project explores how formal methods can make AI systems compliant with complex behavioral requirements without undermining their performance. Our work on liveness shielding develops runtime mechanisms that monitor and guide the behavior of learned or probabilistic policies to ensure that they satisfy rich temporal objectives — not only preventing unsafe behavior, but also guaranteeing that desired goals are eventually achieved. More recently, we extend these ideas to tool-using AI agents driven by large language models. Here, the challenge is to ensure compliance with long and intricate procedural manuals written in natural language. Our recent work develops automated methods for translating such manuals into formally validated compliance checks and symbolic models, enabling scalable verification, benchmarking, and debugging of AI agents operating in realistic environments.

(Past) Group Members Involved:

• Ashwani Anand
• Satya Prakash Nayak
• Ritam Raha
• Anne-Kathrin Schmuck

Publications:

• A. Anand, I. Chatzi, R. Raha, A.-K. Schmuck. MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents. (under review, pre-print)
• * A. Anand, S.P. Nayak, R. Raha, A.-K. Schmuck. Follow the STARs: Dynamic -Regular Shielding of Learned Policies. 2026. AMAAS’26 (preprint, videos)