Flexibility vs. Predictability

Research Question

In a production pipeline with uncontrolled inputs, how does the trade-off between the flexibility of an agentic system and the predictability of a deterministic execution model affect the auditability and formal verification of the system's runtime state?

Findings

Executive Summary

Agentic flexibility reduces exact auditability and full-state formal verifiability unless the system is wrapped in a constrained, trace-rich control shell that records the run well enough to reconstruct what happened and abstracts the workflow into a finite verification target.

Deterministic pipelines also face state-space and observability limits, but current verification tools fit them more naturally because their control flow and update rules are explicit before runtime, which keeps abstraction loss lower and replayability stronger.

Probabilistic model checking shows that stochastic systems are not outside formal methods altogether, yet the tractable object is a finitised Markov-style abstraction such as an MDP rather than the full semantic content of an open-ended agent run.

For regulated production use, the practical design implication is to keep deterministic authority at the final consequential control surface while allowing agentic components upstream only when prompts, retrieval, tool use, outputs, and overrides are durably logged.

Key Findings

1. A production-grade audit trail for an agentic pipeline must capture conversation identity, model identity, prompt and instruction state, retrieval lineage, tool-call lineage, outputs, and errors, because current observability standards and agent-observability literature split those facts across traces, events, attributes, and lifecycle artifacts rather than one canonical log record.
2. The European Union Artificial Intelligence Act's automatic logging requirement means that recorded event traces, not only post hoc textual explanations, are needed where a high-risk system's functioning must later be reconstructed for monitoring or investigation.
3. Current mainstream formal-verification tooling already supports probabilistic and nondeterministic state-transition models such as Markov Decision Processes, so the practical boundary is not randomness by itself but whether an open-ended workflow can be compressed into a finite model with acceptable semantic loss.
4. Deterministic production workflows still face state-space explosion and rely on abstraction, reduction, and compression, but they usually preserve stronger local replayability because explicit guards and updates exist before execution rather than being selected at runtime by a language model.
5. Agentic flexibility expands the relevant runtime state to include prompt content, retrieved data, tool choices, tool outputs, and environment side effects, so the abstraction required for formal verification loses more semantic detail than it typically does in an equivalently scoped deterministic workflow.
6. PRISM says statistical model checking is useful when explicit probabilistic verification becomes infeasible, but is not well suited to models with unresolved nondeterministic choices such as Markov Decision Processes because random paths are not well defined for them.
7. Because agents can misread intent, absorb adversarial instructions through data, and fail to self-correct reliably, trustworthy auditability depends more on durable event lineage than on the model's later narrative or self-reported reasoning.
8. The most defensible production pattern is therefore a hybrid one in which flexible agentic components operate inside bounded tools and telemetry envelopes, while deterministic logic remains authoritative for final approvals, denials, or other consequential state changes.

Assumptions

• Assumption: Formal verification of an agentic pipeline in practice means verification of a finite abstraction of the pipeline rather than full semantic verification of every generated token sequence. Justification: the accessible verifier sources all operate on finitised state-transition models.
• Assumption: Auditability in this item means post hoc reconstruction sufficient for incident review, monitoring, and accountability rather than perfect recovery of latent model intent. Justification: the regulatory and observability sources define traceability through recorded events and reconstruction artefacts.

Analysis

The evidence does not support a simplistic claim that deterministic systems are verifiable and agentic systems are not. PRISM and Storm show that probabilistic and nondeterministic models are legitimate formal-verification targets.

The stronger claim is about semantic distance between the running system and the finite model being verified. Deterministic workflows start from explicit guards, updates, and control flow, so abstraction still loses information, but it usually loses less of the decision surface that matters for audit and replay.

Agentic workflows widen that distance because the branch-driving state includes prompt text, retrieved text, tool options, tool results, and environment-side effects, and some of those surfaces can be adversarial or only partly captured unless the operator deliberately instruments them.

An alternative interpretation is that better models or stronger self-correction could close much of the gap without changing the control pattern. The available evidence does not fully support that alternative, because Huang et al. find unreliable intrinsic self-correction, and the logging requirement in Article 12 still points to event reconstruction rather than trust in model introspection.

The practical equilibrium is therefore hybrid: use formal methods where a bounded finite abstraction exists, use runtime traces to preserve what the abstraction drops, and keep deterministic logic authoritative where the consequence of error or contestation is high.

Risks, Gaps, and Uncertainties

• This item does not quantify a numerical Pareto frontier between flexibility and verifiability, because the accessible sources support a qualitative boundary more strongly than a single cross-system metric.
• The line between acceptable abstraction loss and excessive semantic loss remains domain-specific, especially when external tools mutate the environment.
• The OpenTelemetry generative Artificial Intelligence conventions are still marked as development status, so field names are informative and directionally useful but not yet a settled regulatory schema.

Open Questions

• Which bounded abstraction patterns best preserve the semantics of retrieval and tool choice in enterprise agent pipelines without collapsing tractability?
• What runtime-monitoring or shielding pattern provides the strongest complement to model checking for tool-using agents in mutable environments?
• How should operators measure when an audit trail is reconstructable enough for contestability rather than merely rich enough for debugging?

sources

Consulted:

• [x] Anthropic (2026) Trustworthy agents - agent definition, self-directed loop, and oversight surfaces.
• [x] OpenTelemetry Generative Artificial Intelligence spans - span structure for model calls, tool calls, inputs, outputs, and configuration.
• [x] OpenTelemetry Generative Artificial Intelligence events - event-level capture of request and response details.
• [x] OpenTelemetry Generative Artificial Intelligence attribute registry - canonical fields for conversation, retrieval, tool, and model telemetry.
• [x] European Commission Artificial Intelligence (AI) Act Service Desk Article 12 Record-keeping - accessible text of the EU Artificial Intelligence Act logging and traceability requirement.
• [x] PRISM Probabilistic Model Checker - overview of supported probabilistic verification models and property classes.
• [x] PRISM manual introduction - formal verification framing, supported models, and temporal logics.
• [x] PRISM language introduction - state-based model structure and probabilistic commands.
• [x] PRISM local nondeterminism - explicit treatment of nondeterministic choices in Markov Decision Processes.
• [x] PRISM property specification introduction - supported property languages and quantitative queries.
• [x] PRISM statistical model checking - approximate checking limits on large or nondeterministic models.
• [x] Storm model checker - current probabilistic and partially observable verification targets.
• [x] Holzmann (2003) SPIN Model Checker book extras - explicit-state model-checking topics including abstraction, partial-order reduction, and state compression.
• [x] Dong et al. (2024) AgentOps: Enabling Observability of Large Language Model Agents - peer-reviewed taxonomy of artifacts and data that should be traced through the agent lifecycle.
• [x] Abdelnabi et al. (2023) Indirect Prompt Injection in Large Language Model-Integrated Applications - evidence that uncontrolled data can become executable instruction context.
• [x] Huang et al. (2024) Large Language Models Cannot Self-Correct Reasoning Yet - evidence that intrinsic self-correction is unreliable without external feedback.
• [x] Heim et al. (2025) A Guide to Failure in Machine Learning - reliability and robustness framing for machine-learning failure analysis.
• [x] Mitchell (2026) Research Question 5.1: Stochastic versus Deterministic Failure Modes on Identical Unvalidated Inputs - immediate prior repository item on failure signatures and replayability.
• [x] Mitchell (2026) Are Multi-Step Large Language Model-Based Systems Inherently Less Explainable Than Equivalently Scoped Deterministic Software Systems? - prior repository item on local replayability versus global opacity.
• [x] Mitchell (2026) What observability and telemetry model is required to govern Artificial Intelligence and low-code systems at scale? - prior repository item on governance-grade traceability fields.
• [x] Mitchell (2026) Governance Policy Application: Deterministic Requirements vs Stochastic Large Language Model Elements - prior repository item on deterministic control surfaces in governed decisions.

Identified but not consulted:

• [ ] Clarke et al. (2018) Model Checking, MIT Press - seeded canonical textbook locator checked, but the accessible evidence extracted for this item came from PRISM, Storm, and SPIN documentation plus accessible papers.
• [ ] Baier and Katoen (2008) Principles of Model Checking, MIT Press - seeded canonical textbook locator checked, but the publisher page did not yield extractable content in this environment.