# Agentproof: Static Verification of Agent Workflow Graphs

arXiv: https://arxiv.org/abs/2603.20356 · HTML: https://mlsanity.com/paper/2603.20356/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Mar 2026.

## Built on by (most cited first, 9 of 9)

- [When Agents Do Not Stop: Uncovering Infinite Agentic Loops in LLM Agents](https://mlsanity.com/paper/2607.01641/) (2026)
- [AgentFlow: Building Agent Dependency Graphs for Static Analysis of Agent Programs](https://mlsanity.com/paper/2607.01640/) (2026)
- [Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement](https://mlsanity.com/paper/2608.14590/) (2026)
- [When "Must" Becomes "Maybe": Constraint Weakening in LLM Agent Workflows](https://mlsanity.com/paper/2608.24569/) (2026)
- [CogEEGAgent: Toward Autonomous Cognitive EEG Analysis with Grounded Execution and Selection-Aware Verification](https://mlsanity.com/paper/2607.25045/) (2026)
- [Minimal Oversight: Uncertainty-Aware Governance for Delegated AI Systems](https://mlsanity.com/paper/2606.15563/) (2026)
- [DeFiFlowBench: Benchmarking and Improving Safe Executability in Natural-Language DeFi Workflow Synthesis](https://mlsanity.com/paper/2609.11504/) (2026)
- [Agents as Software: A Programming Languages Agenda for Agent Reliability](https://mlsanity.com/paper/2609.32198/) (2026)
- [SpecGuard: Proving a Task Is Broken Before the Agent Cheats](https://mlsanity.com/paper/2610.09159/) (2026)

## Abstract (arXiv)

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.