diff --git a/crates/aura-cli/src/graph_construct.rs b/crates/aura-cli/src/graph_construct.rs
index a1949eb..add340b 100644
--- a/crates/aura-cli/src/graph_construct.rs
+++ b/crates/aura-cli/src/graph_construct.rs
@@ -85,6 +85,7 @@ fn format_op_error(e: &OpError) -> String {
             format!("kind mismatch {from} -> {to} (producer {producer:?}, consumer {consumer:?})")
         }
         OpError::SlotAlreadyWired { node, slot } => format!("slot {node}.{slot} already wired"),
+        OpError::WouldCycle { from, to } => format!("connecting {from} -> {to} would close a cycle"),
         OpError::BadParam { node, err } => format!("bad param on {node}: {err:?}"),
         OpError::Incomplete(ce) => format!("{ce:?}"),
     }
diff --git a/crates/aura-engine/src/construction.rs b/crates/aura-engine/src/construction.rs
index 97717df..c6f2541 100644
--- a/crates/aura-engine/src/construction.rs
+++ b/crates/aura-engine/src/construction.rs
@@ -59,6 +59,11 @@ pub enum OpError {
     AmbiguousOutPort { node: String, name: String },
     KindMismatch { from: String, to: String, producer: ScalarKind, consumer: ScalarKind },
     SlotAlreadyWired { node: String, slot: String },
+    /// Wiring `from -> to` would close a dataflow cycle among the interior edges:
+    /// `to`'s node already reaches `from`'s node (or it is a self-edge). The only
+    /// legal feedback path is an explicit delay/state node, so a cycle makes the
+    /// blueprint non-acyclic (domain invariant 5 / ledger C9).
+    WouldCycle { from: String, to: String },
     BadParam { node: String, err: BindOpError },
     /// A holistic finalize fault (totality / injectivity / unbound root role),
     /// wrapping the unchanged engine gate's `CompileError`.
@@ -172,6 +177,31 @@ impl<'v> GraphSession<'v> {
         self.names.get(id).copied().ok_or_else(|| OpError::UnknownIdentifier(id.to_string()))
     }
 
+    /// Would adding the interior edge `from_idx -> to_idx` close a dataflow cycle?
+    /// It does iff `to_idx` already reaches `from_idx` through the interior edges
+    /// added so far (or it is a self-edge, the degenerate 1-node loop). Source/input
+    /// role feeds are roots, not interior edges, so they cannot participate. The
+    /// only legal feedback is an explicit delay/state node (domain invariant 5 /
+    /// ledger C9), so this is the acyclicity gate the eager `connect` op enforces.
+    fn closes_cycle(&self, from_idx: usize, to_idx: usize) -> bool {
+        let mut stack = vec![to_idx];
+        let mut seen = HashSet::new();
+        while let Some(n) = stack.pop() {
+            if n == from_idx {
+                return true;
+            }
+            if !seen.insert(n) {
+                continue;
+            }
+            for e in &self.edges {
+                if e.from == n {
+                    stack.push(e.to);
+                }
+            }
+        }
+        false
+    }
+
     /// Mark `(node, slot)` covered, rejecting a second cover eagerly (the >1 arm
     /// of the exactly-once invariant — the holistic 0 arm is deferred to finish).
     fn cover(&mut self, node: usize, node_id: &str, slot: usize, slot_name: &str) -> Result<(), OpError> {
@@ -204,6 +234,9 @@ impl<'v> GraphSession<'v> {
             // can only yield `Ok` or a `KindMismatch`; the index-fault arm is dead.
             _ => unreachable!("edge_kind_check on resolved indices yields only KindMismatch"),
         })?;
+        if self.closes_cycle(fi, ti) {
+            return Err(OpError::WouldCycle { from, to });
+        }
         self.cover(ti, &to_node, slot, &to_slot_name)?;
         self.edges.push(Edge { from: fi, to: ti, slot, from_field });
         Ok(())
@@ -528,6 +561,64 @@ mod tests {
         assert!(!open.iter().any(|(p, _)| p == "sub.lhs"));
     }
 
+    /// DAG invariant (domain invariant 5 / ledger C9): the construction surface
+    /// must reject a dataflow cycle. The only legal feedback path is an explicit
+    /// delay/state node; a `connect` that closes a cycle among interior nodes
+    /// makes the blueprint non-acyclic and must be a construction fault, never a
+    /// silent `Ok`.
+    #[test]
+    fn replay_rejects_dataflow_cycle() {
+        // Mirror fieldtests/cycle-0088-construction-op-script/c0088_3m_two_cycle.json:
+        // two `Sub` nodes a,b each fed `rhs` from price, then a.value->b.lhs and
+        // b.value->a.lhs closing an a<->b 2-cycle. Every interior slot is covered
+        // exactly once and the root role is bound, so every current gate (eager
+        // per-op cover/kind + holistic totality/injectivity/root-boundness) passes
+        // — only an acyclicity check can catch it.
+        let ops = vec![
+            Op::Source { role: "price".into(), kind: ScalarKind::F64 },
+            Op::Add { type_id: "Sub".into(), as_name: Some("a".into()), bind: vec![] },
+            Op::Add { type_id: "Sub".into(), as_name: Some("b".into()), bind: vec![] },
+            Op::Feed { role: "price".into(), into: vec!["a.rhs".into(), "b.rhs".into()] },
+            Op::Connect { from: "a.value".into(), to: "b.lhs".into() }, // op 4: a -> b
+            Op::Connect { from: "b.value".into(), to: "a.lhs".into() }, // op 5: closes b -> a
+            Op::Expose { from: "a.value".into(), as_name: "out".into() },
+        ];
+        let closing_connect = 5;
+        let finalize = ops.len();
+        // `.err()` not `.unwrap_err()`: the Ok arm `Composite` holds build closures
+        // and is not `Debug`.
+        let (idx, _err) = super::replay("g", ops, &aura_std::std_vocabulary)
+            .err()
+            .expect("a cyclic op-list must be rejected (DAG invariant 5 / C9)");
+        // An eager realisation attributes the fault to the closing connect op; a
+        // holistic topological check at finish attributes it to the implicit
+        // finalize index. Accept either so the GREEN side is free to choose.
+        assert!(
+            idx == closing_connect || idx == finalize,
+            "cycle fault should name the closing connect (op {closing_connect}) \
+             or finalize (op {finalize}), got op {idx}"
+        );
+    }
+
+    /// A self-loop (a node feeding its own input) is the degenerate 1-node cycle
+    /// and must be rejected for the same DAG reason (domain invariant 5 / C9).
+    #[test]
+    fn replay_rejects_self_loop() {
+        // single `Sub` s: rhs fed from price, then s.value -> s.lhs closes a 1-node
+        // loop. Both slots covered, role bound — only an acyclicity check catches it.
+        let ops = vec![
+            Op::Source { role: "price".into(), kind: ScalarKind::F64 },
+            Op::Add { type_id: "Sub".into(), as_name: Some("s".into()), bind: vec![] },
+            Op::Feed { role: "price".into(), into: vec!["s.rhs".into()] },
+            Op::Connect { from: "s.value".into(), to: "s.lhs".into() }, // self-edge
+            Op::Expose { from: "s.value".into(), as_name: "out".into() },
+        ];
+        assert!(
+            super::replay("g", ops, &aura_std::std_vocabulary).is_err(),
+            "a self-loop op-list must be rejected (DAG invariant 5 / C9)"
+        );
+    }
+
     #[test]
     fn replay_stops_at_first_failing_op_naming_index() {
         let ops = vec![