Composing Verifiable Conceptual Models via Building Blocks: Towards Design-Time Verification of Agentic AI Workflows¶

🕒 Published (v1): 2026-06-19 16:03 UTC · Source: Arxiv · link

Why this paper was selected

Design-time formal verification of agentic workflows; fills major harness safety gap

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

This paper proposes a design-time verification framework for agentic AI workflows that represents workflows as compositions of reusable behavioral building blocks and checks their structural compatibility via 12 rules before deployment. Unlike runtime guardrails, it detects structural flaws (missing mediators, bypassed appeal paths, unchecked state coupling) at composition time. A software prototype is evaluated on 48 intentionally flawed workflows and 168 structural variants.

Problem¶

Current agentic AI platforms (Claude SDK, LangGraph, CrewAI, AutoGen, etc.) provide only runtime safeguards; none cover all three design-time verification dimensions: schema (structural), behavioral (semantic), and multi-agent coordination. Empirically, 44.2% of agentic system failures trace to poor system design and 23.5% to missing/incorrect verification—yet no tool checks for structural incompatibilities before a workflow is executed.

Method¶

Workflows are formalized as a 6-tuple \(W = (A, S, M, B, E, G)\): agent roles \(A\), state variables \(S\), typed message sets \(M\), behavioral blocks \(B\), execution edges \(E\) (acyclic dependency graph within a cycle), and guards \(G\) (conditional execution predicates). Behavioral blocks are coarse-grained semantic operations (observe, assess, plan, gate, enforce, communicate) rather than concrete actions, enabling reuse. State coupling (writes to persistent agent state) is separated from execution flow to allow feedback without cyclic control graphs. Twelve cross-cutting structural rules are derived from ABM composition best practices (e.g., "a negotiation pattern requires a mediator or decision rule," "an appeal path must not be blocked by the same enforcement action that triggers it"). The verifier is implemented as a software prototype and run against three social-media moderation case studies. Two datasets are used: 48 ground-truth workflows (24 correct, 24 with 1–3 deliberately injected errors) and 168 structural variants that preserve logic but alter graph topology (agent splitting/merging, intermediate nodes).

Key Contributions¶

Formal workflow representation as ABM-inspired compositions of typed behavioral building blocks with explicit state, messages, and guards
A set of 12 structural verification rules targeting recurring design-flaw categories (incompatible block interactions, missing safety gates, bypassed appeal paths, unchecked concurrent state modifications)
A software prototype implementing the rule verifier
Two publicly released datasets (Zenodo DOI provided) covering flawed workflows and topology-preserving structural variants for benchmark reuse
Empirical demonstration that the verifier detects violations even when flaws are obscured by structural transformations such as task-splitting across agents

Results¶

Evaluated on 48 labeled workflows (24 correct / 24 flawed) and 168 structural variants
The verifier reliably detects design violations across the 48 ground-truth workflows (precision, recall, MAE, RMSE reported via confusion matrix—specific numbers cut off in the provided text)
Violations are detected even when flawed designs are refactored through structural transformations (task splitting, agent merging), demonstrating robustness of the rule-based approach
Three case studies (account moderation, Wikipedia edit governance, edit-war dispute resolution) used as reference workflows; each contributes equally to the evaluation set

Limitations¶

Rule set is not claimed to be complete; expanding it requires a larger empirical corpus of real-world agentic workflows and systematic failure analysis
Does not inspect prompt content or tool-invocation semantics—prompt injection, jailbreaks, and malicious retrieved content are out of scope
Does not verify whether individual tool calls are safe, reversible, sandboxed, or authorized at runtime (structural connectivity only)
Rules are checked independently; interactions and conflicts among rules (co-occurring violations) are noted but not fully resolved
Evaluated only on three synthetic case studies from the social-media moderation domain; generalization to other workflow domains is unvalidated

Relevance to Harnesses / Meta-Harnesses¶

This work directly addresses the structural correctness layer that meta-harnesses depend on: a harness that orchestrates multiple LLM agents is itself a workflow, and without design-time verification any compositional flaw propagates silently to runtime. The building-block abstraction (observe → assess → plan → gate → enforce) mirrors how meta-harnesses decompose tasks into reusable phases, making the 12-rule verifier a candidate pre-execution lint step for harness templates. The separation of execution edges from state-coupling graphs is particularly relevant to harnesses that manage shared context stores, where write-order bugs are otherwise invisible until deployment. Future harness tooling could integrate a rule engine of this kind as a "structural type checker" before wiring agents together.