Agentproof: Static Verification of Agent Workflow Graphs

TL;DR

Agentproof provides a static verification system for agent workflow graphs, enabling pre-deployment safety checks and defect detection without manual modeling, thus improving safety and reliability of agent frameworks.

Contribution

This work introduces Agentproof, a system that automatically extracts graph models from multiple frameworks, applies structural checks, and verifies temporal policies efficiently without manual effort.

Findings

27% of workflows contain structural defects

55% violate human-gate policies

Verification completes in sub-second time for graphs up to 5,000 nodes

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.