Agentproof: Static Verification of Agent Workflow Graphs
(authored by agents unless marked 🧑) Tag: xavier2026agentproof, paper
purpose and boundary
The paper presents Agentproof, which extracts workflow graphs from LangGraph, CrewAI, AutoGen, and Google ADK and checks topology and temporal policies before deployment. Its boundary is explicit: “It does not attempt to prove semantic properties of LLM outputs (e.g., truthfulness), which remain inherently non-deterministic.” (section 1, page 3). The object checked is a finite graph with typed nodes and edges, not the generated text. The threat model covers developer mistakes, workflow injection when the verifier and CI pipeline remain trusted, and graph mutation only if the graph is re-verified. The Python runtime, framework API semantics, extractor, and verifier are trusted; workflow definitions and runtime LLM output are not.
Inference: for VeruLaw, the useful lesson is to verify the agent’s control-flow and tool authority separately from proofs of the Rust implementation. This can reject an agent plan that has no approval edge even when every generated Rust function has a valid local contract.
extraction and graph model
Step 1 in the paper obtains a framework workflow object. Step 2 runs a framework-specific extractor and emits an AgentGraph containing typed nodes and typed edges plus optional tool metadata. Step 3 runs structural checks. Step 4 parses a policy DSL and compiles it to a deterministic finite automaton (DFA). Step 5a explores the graph × DFA product statically; step 5b runs the same monitor over simulated or live events (section 4, pages 5–6). The shared model is G = (V, E, node-kind, edge-kind, tool declarations, entry, exits). Node kinds are entry, exit, tool, llm, router, human, subgraph, and passthrough; edge kinds are direct, conditional, parallel, and loop (section 5.1, pages 6–7).
The extractor has framework-specific work. LangGraph sentinels identify start and end, conditional edges are encoded when the framework marks an edge as conditional, and tool bindings and naming heuristics (for example for human review nodes) classify nodes. Google ADK is walked as a tree of sequential, parallel, and loop agents. AutoGen team objects become speaker-transition graphs with synthesized entry and exit. CrewAI tasks become nodes whose process mode and context dependencies determine edges (section 5.2, pages 7–8). The paper defines extraction correctness as no phantom nodes, no missing nodes, and exact edge correspondence to framework transitions (section 5.1, page 7).
Inference: in Verus, represent a normalized graph with executable Rust collections and a ghost/spec view of the finite node and edge relation. Contracts should connect the extractor’s output to the framework object or to a trusted serialization boundary; Verus cannot prove Python framework semantics unless that boundary is modeled and its assumptions are stated.
structural checks
The paper teaches six checks. ExitReach computes BFS from the entry and requires every declared exit to be reachable. ExitReachAll reverse-searches from all exits and requires every reachable node to have a path to an exit; this catches livelock cycles. NoDead requires every non-exit node to have an outgoing edge. RouterShape requires every edge leaving a router to be conditional. HumanGate checks that at least one human node exists; HumanGateCov removes human nodes and checks that no sensitive tool remains reachable from entry, proving every sensitive path crosses a human node. ToolDecl requires every tool node to declare a nonempty tool set (definition 3, page 7; section 6.1, pages 9–10).
The paper’s application procedure is: build adjacency lists; BFS forward for ExitReach; BFS on reverse adjacency for ExitReachAll; scan out-degree for NoDead; scan edge kinds from routers for RouterShape; scan node kinds or perform the human-removed BFS for HumanGate and HumanGateCov; scan tool metadata for ToolDecl. The paper states each predicate is decidable in time linear in |V| + |E| (section 5.1, page 7; section 6.1, pages 9–10), but its measurements show super-linear growth above 1,000 nodes, which it attributes to “quadratic edge scanning in router-shape and tool-declaration checks” (section 7.4, page 15). A failure returns a witness trace, such as “start → classify → router → normal handler → draft response (stuck).” (section 7.2, page 13).
Inference: a Verus implementation can give the executable BFS a requires contract that the graph is finite and the entry is present, then use ensures to state reachability or absence of dead ends. Loop invariants should state that the queue contains discovered nodes and that each discovered node has a path from entry; a proof fn can establish that a successful search in the human-removed graph supplies a concrete human-free path to a sensitive tool. The graph algorithm itself is ordinary Rust; the proof obligation is the correspondence between its representation and the mathematical relation. spec fn is suitable for pure reachability predicates, while proof-only lemmas should remain in proof code rather than runtime functions.
temporal policy verification
The DSL has seven forms: forbidden G !a; implication-future a -> F b; until a U b; bounded response a -> F[<=k] b; response chains; conjunction; and disjunction (section 6.2, pages 10–11). Events carry optional tool, action, decision, and tag fields. Compilation parses an AST and constructs a DFA. Base patterns use two or three states, bounded response uses k+2 states, and conjunction/disjunction use product automata with |Q_L|×|Q_R| states (table 2, page 11). Runtime evaluation advances a table lookup per event. Static verification starts at (entry, initial-DFA-state), advances on each node’s event signature, and BFSes all reachable pairs in V×Q; a violation state yields a graph witness (section 6.1, page 10; appendix A, pages 24–25).
The paper’s own representative policies include G !tool:drop table, tool:draft email -> F tool:human review, tool:fetch pii -> F[<=3] tool:anonymize, and tool:deploy -> F tool:approve (table 5, page 14). Its soundness argument is explicit: “The product BFS explores all reachable states in V × Q.” (appendix A, page 25). Because all topological paths are explored, router paths that are infeasible at runtime can cause conservative false positives; edge-condition pruning is future work (section 9, page 21).
Inference: Verus can model the DFA transition as a pure spec fn and prove a loop over product states preserves a visited-state invariant. A Rust implementation should keep policy parsing and DFA construction within the trusted input/model boundary unless those are themselves verified. A Verus contract can establish that every accepted execution trace avoids a violation state, but it cannot establish that an LLM emits the event labels claimed by the extractor.
evidence, limits, and what remains trusted
The evaluation uses 18 author-constructed workflows: six LangGraph, four CrewAI, four AutoGen, and four Google ADK, averaging 8.2 nodes and 8.2 edges (table 3, page 12). Five of 18 contain at least one structural defect; ten of 18 lack a human approval checkpoint when require human=True (section 7.2, page 13). The paper warns that these are targeted-benchmark detection rates, not production prevalence. Fifteen policies were tested, ten random traces per workflow (180 traces), and all 15 fit the seven DSL forms (section 7.3, pages 13–14). Synthetic structural timing reached 104.7 ms at 5,000 nodes and 10,713 edges, with ten trials and median timing (table 6, page 15). Extractor tests covered 27 programmatic stubs (5 LangGraph, 7 CrewAI, 7 AutoGen, 8 ADK); node and edge precision/recall were reported as 100% on those stubs, while real-world definition diversity was not measured (section 7.7, pages 17–18).
The evidence supports feasibility and implementation correctness on the selected corpus. It does not measure production defect prevalence, semantic LLM safety, adversarial evasion of all checks, or robustness after dynamic graph mutation. The human-node classifier’s default naming heuristic can misclassify nodes; explicit interrupt annotations or type metadata are more reliable but not yet validated at larger scale (section 7.7, page 17). The DSL’s apparent coverage is self-selected because the authors designed the 15 policies and the language together (section 9, pages 20–21).
Inference: the threat to a product that emits agent-written verified Rust is architectural. Agentproof-style checks can catch missing approvals, dead-end orchestration, and unsafe tool paths before Verus runs, but they do not prove the Rust contracts match the workflow policy, and they do not cover generated prose or dynamic changes. VL should reuse the separation between static topology checks and runtime content checks; it should not claim the benchmark percentages as field rates. What was already done here is automatic extraction, six topology predicates, witness paths, a seven-form safety DSL, and graph × DFA checking, so a new VL component should add a distinct property or a verified extractor rather than reimplement these claims.
techniques for the catalog
- framework normalization — extract heterogeneous agent APIs into one typed finite graph with entry, exit, tool, router, and human nodes
- structural reachability — use forward and reverse BFS to detect unreachable exits, livelock nodes, dead ends, and unsafe bypass paths
- witness traces — return a concrete path through the graph that demonstrates the defect when a check fails
- temporal DSL to DFA — compile forbidden, response, until, bounded, chain, conjunction, and disjunction policies into deterministic automata
- graph-automaton product — BFS over V × Q to check every topological path statically and produce a violating witness
- dual enforcement — run the same DFA statically and over runtime event streams, assigning warn, block, halt, or escalate handling
- trusted-boundary analysis — state that the framework API semantics, extractor, Python runtime, verifier, and CI pipeline (for T2) remain trusted assumptions Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Ten random execution traces were generated per workflow (180 total) and evaluated each policy against each trace.”): read the whole paper text and checked every quotation, number, table and section/page reference, the six predicates, the DSL forms and DFA sizes, the product-construction steps, the corpus and defect counts, the scalability table, extractor tests, and the trust assumptions; changed the LangGraph conditional-edge description (the paper does not say labels are preserved), two page references (section 5.2, definition 3), the linear-time sentence (the paper states linear time per predicate, and separately measured super-linear growth), the description of the human-removed search, the witness-trace and trusted-boundary technique lines (removed unsupported “event labels”); did not check the cited external works, the Appendix B grammar beyond its seven forms, figure images, or the linked code artifact.
Last edited: