Agentproof: Static Verification of Agent Workflow Graphs

• URL: http://arxiv.org/abs/2603.20356v1
• Date: Fri, 20 Mar 2026 13:56:20 GMT
• Title: Agentproof: Static Verification of Agent Workflow Graphs
• Abstract summary: Agent frameworks increasingly encode tool-using behavior as explicit workflow graphs, yet safety enforcement remains a runtime concern.<n>This paper presents Agentproof, a system that automatically extracts a unified abstract graph model from four major agent frameworks.<n>Unlike general-purpose model checkers, Agentproof requires no manual modeling.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Agent frameworks increasingly encode tool-using behavior as explicit workflow graphs, yet safety enforcement remains a runtime concern. These frameworks expose analyzable graph structure through their APIs, enabling pre-deployment static verification of safety properties that runtime guardrails can only check reactively. This paper presents Agentproof, a system that automatically extracts a unified abstract graph model from four major agent frameworks (LangGraph, CrewAI, AutoGen, Google ADK), applies six structural checks with witness trace generation, and evaluates temporal safety policies via a DSL compiled to deterministic finite automata, both statically through a graph x DFA product construction and at runtime over event traces. Unlike general-purpose model checkers, Agentproof requires no manual modeling. In a curated benchmark of 18 author-constructed workflows, 27% of the benchmark contain structural defects (dead-end nodes, unreachable exits) and 55% violate a human-gate policy when enforced, distinct categories that prior work conflates. All 15 temporal policies defined fit within the seven-form DSL fragment, and verification completes in sub-second time for graphs up to 5,000 nodes. The corpus serves as a reproducible benchmark for evaluating static verification tools rather than as a prevalence study; defect rates reflect tool detection capability on a targeted benchmark, not base rates in production systems. Nonetheless, static graph verification complements runtime guardrails by catching topology-level defects that runtime tools miss unless the offending path is exercised.

Related papers

• Automating Attack Graph Construction for Agentic Pentesting. Towards Neuro-Symbolic Vulnerability Hunting [0.0]
  Logic attack graphs grounded in scanner output provide explicit and auditable attack path reasoning.<n>Integrating symbolic frameworks such as MulVAL to contemporary security or agentic pipelines requires translating scanner evidence to initial facts.<n>We present a semi-automated pipeline that addresses this interoperability problem and depict its feasibility in a web-security case study.
  arXiv  Detail & Related papers  (2026-09-14T13:13:54Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• ScrambleToolBench: Agents Search Exhaustively Even When Their Own Map Points to the Next Step [74.83535434786145]
  We introduce ScrambleToolBench, an interactive terminal benchmark designed to isolate behavioral reasoning.<n>The benchmark requires agents to uncover hidden tool behaviors entirely through trial-and-error interaction.<n>Our evaluation of state-of-the-art language models reveals that successful initial discovery does not translate into robust adaptation.
  arXiv  Detail & Related papers  (2026-08-03T15:07:46Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• ClawForge: Generating Executable Interactive Benchmarks for Command-Line Agents [59.626170560327274]
  We present textbfClawForge, a generator-backed benchmark framework for executable command-line categories under state conflict.<n>We instantiate this framework as the ClawForge-Bench (17 scenarios, 6 ability categories)
  arXiv  Detail & Related papers  (2026-05-13T21:34:08Z)
• Willful Disobedience: Automatically Detecting Failures in Agentic Traces [2.2365938060262356]
  AgentPex is an AI-powered tool designed to systematically evaluate agentic traces.<n>It extracts behavioral rules from agent prompts and system instructions, then uses these specifications to automatically evaluate traces for compliance.<n>We evaluate AgentPex on 424 traces from 2-bench across models in telecom, retail, and airline customer service.
  arXiv  Detail & Related papers  (2026-03-25T00:33:39Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• An End-to-End Framework for Functionality-Embedded Provenance Graph Construction and Threat Interpretation [2.0740117800511215]
  Auto-Prov is an end-to-end framework for provenance graph-based anomaly detectors.<n>It clusters unseen log types and efficiently extracts provenance edges and entity-level information.<n>It infers system-level functional context for both known and previously unseen system entities.<n>It produces stable, interpretable attack summaries that remain robust under system evolution.
  arXiv  Detail & Related papers  (2026-03-17T19:40:05Z)
• AgentProcessBench: Diagnosing Step-Level Process Quality in Tool-Using Agents [50.481033105867205]
  We introduce AgentProcessBench, the first benchmark dedicated to evaluating step-level effectiveness in realistic, tool-augmented trajectories.<n>The benchmark comprises 1,000 diverse trajectories and 8,509 human-labeled step annotations with 89.1% inter-annotator agreement.<n>It features a ternary labeling scheme to capture exploration and an error propagation rule to reduce labeling ambiguity.
  arXiv  Detail & Related papers  (2026-03-15T16:13:58Z)
• FP-Predictor - False Positive Prediction for Static Analysis Reports [5.4164223824711755]
  This work presents a Graph Convolutional Network (GCN) model designed to predict Static Application Security Testing (SAST) reports as true and false positive.<n>The model leverages Code Property Graphs (CPGs) constructed from static analysis results to capture both, structural and semantic relationships within code.<n> Evaluation on the CryptoAPI-Bench benchmark demonstrated the model's practical applicability, reaching an overall accuracy of up to 96.6%.
  arXiv  Detail & Related papers  (2026-03-11T09:05:39Z)
• GraphBit: A Graph-based Agentic Framework for Non-Linear Agent Orchestration [34.588097323063074]
  GraphBit is an engine-orchestrated framework that defines explicitly and deterministically as a directed acyclic graph (DAG)<n>Unlike prompted orchestration, agents in GraphBit operate as typed functions, while a Rust-based engine governs routing, state transitions, and tool invocation, ensuring auditability.<n>A three-tier memory architecture consisting of ephemeral scratch space, structured state, and external connectors isolates context across stages, preventing cascading context that degrades reasoning in long-running pipelines.
  arXiv  Detail & Related papers  (2026-03-08T18:32:28Z)
• ESAA: Event Sourcing for Autonomous Agents in LLM-Based Software Engineering [0.0]
  This paper presents the ESAA (Event Sourcing for Autonomous Agents) architecture.<n>The architecture separates the cognitive intention from the project's state mutation, inspired by the Event Sourcing pattern.<n>Two case studies validate the architecture, providing empirical evidence of the architecture's scalability beyond single-agent scenarios.
  arXiv  Detail & Related papers  (2026-02-26T16:45:59Z)
• CaMeLs Can Use Computers Too: System-level Security for Computer Use Agents [60.98294016925157]
  AI agents are vulnerable to prompt injection attacks, where malicious content hijacks agent behavior to steal credentials or cause financial loss.<n>We introduce Single-Shot Planning for CUAs, where a trusted planner generates a complete execution graph with conditional branches before any observation of potentially malicious content.<n>Although this architectural isolation successfully prevents instruction injections, we show that additional measures are needed to prevent Branch Steering attacks.
  arXiv  Detail & Related papers  (2026-01-14T23:06:35Z)
• BackdoorAgent: A Unified Framework for Backdoor Attacks on LLM-based Agents [58.83028403414688]
  Large language model (LLM) agents execute tasks through multi-step workflow that combine planning, memory, and tool use.<n>Backdoor triggers injected into specific stages of an agent workflow can persist through multiple intermediate states and adversely influence downstream outputs.<n>We propose textbfBackdoorAgent, a modular and stage-aware framework that provides a unified agent-centric view of backdoor threats in LLM agents.
  arXiv  Detail & Related papers  (2026-01-08T03:49:39Z)
• AgentArmor: Enforcing Program Analysis on Agent Runtime Trace to Defend Against Prompt Injection [14.522205401511727]
  Large Language Model (LLM) agents offer a powerful new paradigm for solving various problems by combining natural language reasoning with the execution of external tools.<n>In this work, we propose a novel insight that treats the agent runtime traces as structured programs with analyzable semantics.<n>We present AgentArmor, a program analysis framework that converts agent traces into graph intermediate representation-based structured program dependency representations.
  arXiv  Detail & Related papers  (2025-08-02T07:59:34Z)
• DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
  Large Language Models (LLMs) are increasingly central to agentic systems due to their strong reasoning and planning capabilities.<n>This interaction also introduces the risk of prompt injection attacks, where malicious inputs from external sources can mislead the agent's behavior.<n>We propose a Dynamic Rule-based Isolation Framework for Trustworthy agentic systems, which enforces both control and data-level constraints.
  arXiv  Detail & Related papers  (2025-06-13T05:01:09Z)
• SOPBench: Evaluating Language Agents at Following Standard Operating Procedures and Constraints [59.645885492637845]
  SOPBench is an evaluation pipeline that transforms each service-specific SOP code program into a directed graph of executable functions.<n>Our approach transforms each service-specific SOP code program into a directed graph of executable functions and requires agents to call these functions based on natural language SOP descriptions.<n>We evaluate 18 leading models, and results show the task is challenging even for top-tier models.
  arXiv  Detail & Related papers  (2025-03-11T17:53:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.