Skip to content

Author

Divyakumar Deepak Savla

2 papers indexed here

We haven’t gathered this author’s papers yet. Follow them and we’ll fetch their work.

Not the right person? Other researchers publish under this name.

Conference Aug 2026

MCSafe-GSN-HOL: A Formal Assurance Framework for Machine-Checkable Safety Cases of Deployed LLM Agents

Deployed large language model (LLM) agents are now being used to interface with external tools, fetch information, run code, interact with user data and help with decision making at the workflow level. Therefore, their safety issues are not only related to the underlying model, but also to tool permissions, prompt design, retrieval sources, policy constraints, evidence validity, and varying operational contexts. While Goal Structuring Notation (GSN) has become a popular means of structuring safety arguments, many GSN-based safety cases are still reliant on manual inspection and can suffer from unsupported goals, incomplete evidence paths, undischarged assumptions, circular arguments, unaddressed defeaters, or insufficient coverage of hazards. This paper introduces MCSafe-GSN-HOL, a formal assurance framework for creating machine-checkable safety cases for deployed LLM agents that overcomes these disadvantages. The proposed framework translates the structured GSN arguments into Isabelle/HOL proof obligations, and formalizes the typed GSN elements, the hazard contracts of LLM-agents, the evidence-completeness conditions, the assumption-discharge rules, the defeater-resolution rules, and the incremental re-verification rules after deployment changes. The prototype was tested with 25 safety-case fragments from five representative scenarios of LLM-agents. Results demonstrate that MCSafe-GSN-HOL has 97.3% defect detection, 97.2% evidence coverage, 96.4% hazard-control coverage, and 62.7% reduction in review time compared to manual GSN review. The mean Isabelle/HOL checking time was 2.53 s/safety case, showing that theorem-prover supported assurance can still be practical for medium scale safety-case checking. The results overall support the conclusion that formally checked GSN safety cases can help with the traceability, auditability, consistency and maintainability of assurance processes for deployed LLM-agent systems.

Aakash Abhay Yadav, Shashank Shelat, B. Hinduja et al. · 0 citations
Conference Aug 2026

Reconceptualizing Observability for Agentic AI Systems: A Trace-Centric Architecture for Interpreting Non-Deterministic Workflow Behavior

The more typical feature of agentic AI systems is dynamic, multistep workflows where autonomous components plan, reason, and communicate with external tools and data sources in a series of iterations. Such flexibility increases capability but also brings nondeterminism which is inherent and where the same inputs can result in different execution paths and outputs. The variability creates a major challenge to the traditional observability approaches that are mostly created to support deterministic and service-oriented architectures. This paper redefines observability as an architectural element and introduces a trace-oriented architecture to suit agentic processes. The suggested solution presents semantically rich trace units capturing reasoning transitions, the intent to select a tool, the evolution of memory, and policy interactions, to gain a better insight into the execution behaviour. One of the major innovations is the combination of branch-aware trace modelling with an adaptive fidelity mechanism to dynamically change monitoring granularity based on uncertainty and anomaly indicators. Experimental analysis of various agent workflows shows significant increases in completeness of traces, accuracy in detection of anomalies and localization of root-cause, and a significant decrease in diagnosis time. The findings suggest that the suggested architecture does not only increase interpretability but also helps to ensure the reliable and efficient functioning of non-deterministic AI systems.

Ankur Gupta, Karan Gupta, Divyakumar Deepak Savla et al. · 0 citations