Defensive Publication: Deterministic Forward-Only Decision-Gated Workflow Chains with Both-Branch Coverage Proofs

Abstract

A method for structuring an automated, receipted computation workflow ("chain") as a directed, forward-only sequence of deterministic computation steps interspersed with decision gates, where each gate is constrained to be a total function over previously recorded step outputs (no free-form expression language, no loops, no backward jumps), each gate declares a mandatory default branch, and the chain definition itself carries a machine-checkable proof that both the true and false branches of every gate are reachable and lead to a terminal state. This yields workflows whose control flow is fully enumerable and auditable ahead of execution, rather than only reconstructible after the fact from logs.

Field and problem

Business-process and workflow-automation systems (BPMN engines, serverless step functions, LLM-agent orchestration frameworks) commonly allow arbitrary conditional expressions, loops, and dynamic branching driven by opaque logic (including LLM output) to decide what happens next. This makes two things hard to guarantee ahead of time: (1) that the workflow terminates, since loops and backward jumps can produce non-terminating or state-dependent paths; and (2) that every possible outcome of a decision point has been anticipated and leads somewhere defined, since branch coverage is typically verified only empirically (by testing) rather than structurally (by proof over the chain definition itself).

Detailed description of the novel mechanism

1. Chain shape. A chain is defined as a directed acyclic sequence of nodes. Each node is either a compute step (a pure, receipted function call whose output is recorded as a payload) or a decision gate.
2. Gate constraint - total function only. A decision gate's condition is restricted to a total function over the recorded output_payload fields of prior steps in the same chain - e.g. a comparison, a membership test, or a boolean combination thereof. The gate is explicitly disallowed from containing: a general-purpose expression language, a loop construct, external I/O, or a backward reference to a node later than itself in execution order. This restriction is what makes the full branch structure enumerable by static inspection of the chain definition, without running it.
3. Mandatory default. Every gate must declare an explicit default branch that is taken when its condition evaluates in a way not otherwise covered (or, in the boolean case, both true and false are explicit named branches - there is no implicit "else falls through to nothing").
4. Both-branch coverage proof. The chain definition includes, or can generate, a coverage proof: for every gate in the chain, both declared branches are shown (by static graph traversal, not by execution) to lead to a terminal node of the chain - i.e. neither branch is a dead end and neither branch re-enters a state already visited (enforcing forward-only, acyclic flow). A chain that fails this proof is rejected before it is ever run.
5. Forward-only execution. At runtime, the chain executes nodes in the order fixed by the (already coverage-proved) chain definition. Because gates can only read already-recorded outputs and never jump backward, the executed path is always a subset of the statically enumerated paths - there is no way for the running chain to enter a state the coverage proof did not already account for.
6. Receipt linkage. Each executed node (compute step or gate) produces a receipt entry recording its inputs, output, and (for gates) which branch was taken. Because the chain definition is itself content-hashed, a verifier can confirm the executed path is consistent with a specific, previously coverage-proved chain definition - not an ad hoc, undocumented control-flow path.

Variations

• Gate conditions may be expressed as a small closed set of typed comparators (numeric threshold, string equality, set membership, boolean AND/OR/NOT of the above) rather than a single comparator type, provided the closed set remains statically enumerable.
• The coverage proof may be computed at chain-authoring time (and cached alongside the chain definition) or recomputed at each execution as a pre-flight check; both satisfy the same invariant.
• Terminal nodes may themselves be typed (e.g. "approved", "declined", "escalate-to-human") so the coverage proof also certifies that every gate path resolves to one of a known, finite set of outcome classes.
• Multiple gates may share the same upstream compute step's output without violating the forward-only constraint, since sharing a read does not introduce a cycle.

Prior-art context

BPMN and general workflow engines support conditional branching but typically permit arbitrary expression evaluation, external calls within conditions, and loop/gateway constructs whose full branch space is not required to be statically proved reachable-and-terminal before deployment. Static program-analysis techniques (e.g. control-flow graph reachability) are well known in software verification generally, but this disclosure is specific to their application as a mandatory, pre-execution admission gate for a receipted computation-chain product, tied to a restricted total-function-only gate grammar and coupled to a content-hashed, receipt-verifiable chain definition.