diff --git a/proptest-regressions/ir/cycle_analyse_tests.txt b/proptest-regressions/ir/cycle_analyse_tests.txt
new file mode 100644
index 00000000..9a317216
--- /dev/null
+++ b/proptest-regressions/ir/cycle_analyse_tests.txt
@@ -0,0 +1,7 @@
+# Seeds for failure cases proptest has generated in the past. It is
+# automatically read and these particular cases re-run before any
+# novel cases are generated.
+#
+# It is recommended to check this file in to source control so that
+# everyone who runs the test benefits from these saved cases.
+cc 640655db179ded3e45892515bc53016a7193ab2527ac7b78216b7117358d4b77 # shrinks to (count, edges) = (2, [])
diff --git a/src/ir/cmd_interpolate.rs b/src/ir/cmd_interpolate.rs
index edd91e90..c621999c 100644
--- a/src/ir/cmd_interpolate.rs
+++ b/src/ir/cmd_interpolate.rs
@@ -265,4 +265,69 @@ mod tests {
         .expect("command");
         assert_eq!(command, "in out out");
     }
+
+    mod property_tests {
+        use super::*;
+        use proptest::prelude::*;
+
+        /// Strategy producing short, shell-safe path lists.
+        fn path_list(max: usize) -> impl Strategy<Value = Vec<Utf8PathBuf>> {
+            proptest::collection::vec("[a-z][a-z0-9]{0,5}", 1..=max)
+                .prop_map(|names| names.into_iter().map(Utf8PathBuf::from).collect())
+        }
+
+        fn token() -> impl Strategy<Value = &'static str> {
+            prop_oneof![
+                Just("$in"),
+                Just("$out"),
+                Just("__NETSUKE_INS_PLACEHOLDER__"),
+                Just("__NETSUKE_OUTS_PLACEHOLDER__"),
+            ]
+        }
+
+        proptest! {
+            /// Tokens inside backtick-delimited regions are never substituted
+            /// and survive verbatim.
+            #[test]
+            fn tokens_inside_backticks_are_preserved_verbatim(
+                ins in path_list(3),
+                outs in path_list(3),
+                guarded in token(),
+            ) {
+                let template = format!("echo `{guarded}` done");
+                let command = interpolate_command(&template, &ins, &outs)
+                    .map_err(|e| TestCaseError::fail(format!("interpolation failed: {e}")))?;
+                prop_assert_eq!(command, template);
+            }
+
+            /// Placeholder tokens outside backticks are always replaced with
+            /// the joined input and output lists.
+            #[test]
+            fn placeholders_outside_backticks_are_always_replaced(
+                ins in path_list(3),
+                outs in path_list(3),
+            ) {
+                let command = interpolate_command(
+                    "cp __NETSUKE_INS_PLACEHOLDER__ __NETSUKE_OUTS_PLACEHOLDER__",
+                    &ins,
+                    &outs,
+                )
+                .map_err(|e| TestCaseError::fail(format!("interpolation failed: {e}")))?;
+                let join = |paths: &[Utf8PathBuf]| {
+                    paths
+                        .iter()
+                        .map(|path| path.as_str())
+                        .collect::<Vec<_>>()
+                        .join(" ")
+                };
+                let expected = format!("cp {} {}", join(&ins), join(&outs));
+                prop_assert_eq!(&command, &expected);
+                prop_assert!(
+                    !command.contains("PLACEHOLDER"),
+                    "placeholder survived substitution: {}",
+                    command
+                );
+            }
+        }
+    }
 }
diff --git a/src/ir/cycle_analyse_tests.rs b/src/ir/cycle_analyse_tests.rs
index b5cddd5a..2f8ffaed 100644
--- a/src/ir/cycle_analyse_tests.rs
+++ b/src/ir/cycle_analyse_tests.rs
@@ -170,3 +170,160 @@ proptest! {
         );
     }
 }
+
+/// Build a graph of `count` nodes with the given forward `(from, to)` edges.
+///
+/// Forward edges (`to > from`) cannot create back-edges, so the result is a
+/// directed acyclic graph by construction.
+fn make_forward_edge_graph(
+    count: usize,
+    edges: &[(usize, usize)],
+) -> HashMap<camino::Utf8PathBuf, super::super::super::BuildEdge> {
+    let nodes = sequential_nodes(count);
+    let mut inputs: Vec<Vec<camino::Utf8PathBuf>> = vec![Vec::new(); count];
+    for &(from, to) in edges {
+        if to > from
+            && let (Some(target), Some(dep)) = (inputs.get_mut(from), nodes.get(to))
+        {
+            target.push(dep.clone());
+        }
+    }
+    nodes
+        .iter()
+        .zip(inputs)
+        .map(|(name, deps)| {
+            let mut builder = EdgeBuilder::new(name.clone());
+            for dep in deps {
+                builder = builder.input(dep);
+            }
+            (name.clone(), builder.build())
+        })
+        .collect()
+}
+
+proptest! {
+    /// A graph with no back-edges never produces a cycle, regardless of node
+    /// count or edge layout.
+    #[test]
+    fn forward_edge_graphs_never_report_cycles(
+        (count, edges) in (2usize..=8).prop_flat_map(|count| {
+            (
+                Just(count),
+                proptest::collection::vec((0..count, 0..count), 0..=count * 2),
+            )
+        }),
+    ) {
+        let targets = make_forward_edge_graph(count, &edges);
+        let report = analyse(&targets);
+        prop_assert!(report.cycle.is_none(), "unexpected cycle: {:?}", report.cycle);
+    }
+
+    /// Any graph containing a back-edge always produces a cycle, even with
+    /// extra forward edges layered on top.
+    #[test]
+    fn back_edge_graphs_always_report_cycles(
+        (count, edges) in (2usize..=8).prop_flat_map(|count| {
+            (
+                Just(count),
+                proptest::collection::vec((0..count, 0..count), 0..=count),
+            )
+        }),
+    ) {
+        let nodes = sequential_nodes(count);
+        // Guarantee a path from the first node to the last by including the
+        // chain edges alongside the random forward edges, then close the
+        // loop with a back-edge from the last node to the first.
+        let mut all_edges = edges;
+        all_edges.extend((0..count - 1).map(|i| (i, i + 1)));
+        let mut targets = make_forward_edge_graph(count, &all_edges);
+        let (Some(last), Some(first)) = (nodes.last(), nodes.first()) else {
+            prop_assert!(false, "graph requires at least two nodes");
+            return Ok(());
+        };
+        let builder = EdgeBuilder::new(last.clone()).input(first.clone());
+        targets.insert(last.clone(), builder.build());
+        let report = analyse(&targets);
+        prop_assert!(report.cycle.is_some(), "expected a cycle to be reported");
+    }
+
+    /// Missing-dependency records are exactly the edges whose targets are
+    /// absent from the target map.
+    #[test]
+    fn missing_dependencies_match_absent_edge_targets(
+        (count, ghost_edges) in (2usize..=6).prop_flat_map(|count| {
+            (
+                Just(count),
+                proptest::collection::hash_set((0..count, 0..3usize), 0..=count),
+            )
+        }),
+    ) {
+        let nodes = sequential_nodes(count);
+        let mut targets = make_acyclic_chain(&nodes);
+        let mut expected: Vec<(camino::Utf8PathBuf, camino::Utf8PathBuf)> = Vec::new();
+        for &(node_idx, ghost_idx) in &ghost_edges {
+            let ghost = path(&format!("ghost{ghost_idx}"));
+            let Some(name) = nodes.get(node_idx).cloned() else {
+                prop_assert!(false, "node index out of range");
+                return Ok(());
+            };
+            let Some(edge) = targets.remove(&name) else {
+                prop_assert!(false, "node should exist");
+                return Ok(());
+            };
+            let mut builder = EdgeBuilder::new(name.clone()).implicit_dep(ghost.clone());
+            for input in edge.inputs {
+                builder = builder.input(input);
+            }
+            for dep in edge.implicit_deps {
+                builder = builder.implicit_dep(dep);
+            }
+            targets.insert(name.clone(), builder.build());
+            expected.push((name, ghost));
+        }
+        let report = analyse(&targets);
+        prop_assert!(report.cycle.is_none());
+        let mut reported = report.missing_dependencies;
+        reported.sort();
+        expected.sort();
+        for (dependent, missing) in &reported {
+            prop_assert!(targets.contains_key(dependent));
+            prop_assert!(!targets.contains_key(missing));
+        }
+        prop_assert_eq!(reported, expected);
+    }
+
+    /// Results are stable across arbitrary `HashMap` insertion orderings.
+    #[test]
+    fn analyse_is_stable_across_insertion_orders(
+        (count, order) in (2usize..=6).prop_flat_map(|count| {
+            (
+                Just(count),
+                Just((0..count).collect::<Vec<_>>()).prop_shuffle(),
+            )
+        }),
+    ) {
+        let nodes = sequential_nodes(count);
+        let canonical = make_cycle_graph(&nodes);
+        let baseline = analyse(&canonical);
+
+        let mut shuffled = HashMap::new();
+        for index in order {
+            let Some(name) = nodes.get(index).cloned() else {
+                prop_assert!(false, "node index out of range");
+                return Ok(());
+            };
+            let Some(edge) = canonical.get(&name) else {
+                prop_assert!(false, "node should exist");
+                return Ok(());
+            };
+            shuffled.insert(name, edge.clone());
+        }
+        let report = analyse(&shuffled);
+        prop_assert_eq!(report.cycle, baseline.cycle);
+        let mut left = report.missing_dependencies;
+        let mut right = baseline.missing_dependencies;
+        left.sort();
+        right.sort();
+        prop_assert_eq!(left, right);
+    }
+}
diff --git a/tests/ninja_property_tests.rs b/tests/ninja_property_tests.rs
new file mode 100644
index 00000000..6ccf481f
--- /dev/null
+++ b/tests/ninja_property_tests.rs
@@ -0,0 +1,108 @@
+//! Property-based tests for Ninja build-line separator ordering.
+//!
+//! PR #315 established the separator contract for generated build lines:
+//! explicit inputs, then `|` implicit dependencies, then `||` order-only
+//! dependencies. These tests pin that ordering across generated dependency
+//! lists.
+
+use netsuke::ast::Recipe;
+use netsuke::ir::{Action, BuildEdge, BuildGraph};
+use proptest::prelude::*;
+use proptest::test_runner::TestCaseError;
+use std::collections::HashMap;
+
+fn paths(values: &[String]) -> Vec<camino::Utf8PathBuf> {
+    values.iter().map(camino::Utf8PathBuf::from).collect()
+}
+
+fn graph_with_edge(
+    inputs: &[String],
+    implicit_deps: &[String],
+    order_only_deps: &[String],
+) -> BuildGraph {
+    let action = Action {
+        recipe: Recipe::Command {
+            command: "touch out".into(),
+        },
+        description: None,
+        depfile: None,
+        deps_format: None,
+        pool: None,
+        restat: false,
+    };
+    let edge = BuildEdge {
+        action_id: "act".into(),
+        inputs: paths(inputs),
+        implicit_deps: paths(implicit_deps),
+        explicit_outputs: vec!["out".into()],
+        implicit_outputs: Vec::new(),
+        order_only_deps: paths(order_only_deps),
+        phony: false,
+        always: false,
+    };
+    let mut actions = HashMap::new();
+    actions.insert("act".to_owned(), action);
+    let mut targets = HashMap::new();
+    targets.insert(camino::Utf8PathBuf::from("out"), edge);
+    BuildGraph {
+        actions,
+        targets,
+        default_targets: Vec::new(),
+    }
+}
+
+fn build_line(
+    inputs: &[String],
+    implicit_deps: &[String],
+    order_only_deps: &[String],
+) -> Result<String, TestCaseError> {
+    let graph = graph_with_edge(inputs, implicit_deps, order_only_deps);
+    let ninja = netsuke::ninja_gen::generate(&graph)
+        .map_err(|e| TestCaseError::fail(format!("generate failed: {e}")))?;
+    ninja
+        .lines()
+        .find(|line| line.starts_with("build "))
+        .map(str::to_owned)
+        .ok_or_else(|| TestCaseError::fail(format!("no build line in:\n{ninja}")))
+}
+
+fn name_list(max: usize) -> impl Strategy<Value = Vec<String>> {
+    proptest::collection::vec("[a-z][a-z0-9]{0,7}", 1..=max)
+}
+
+proptest! {
+    /// With all three dependency classes present, the emitted line always
+    /// places `|` after explicit inputs and before `||`.
+    #[test]
+    fn separators_follow_inputs_then_implicit_then_order_only(
+        inputs in name_list(4),
+        implicit in name_list(4),
+        order_only in name_list(4),
+    ) {
+        let line = build_line(&inputs, &implicit, &order_only)?;
+        let expected = format!(
+            "build out: act {} | {} || {}",
+            inputs.join(" "),
+            implicit.join(" "),
+            order_only.join(" "),
+        );
+        prop_assert_eq!(line, expected);
+    }
+
+    /// The `|` separator is absent when `implicit_deps` is empty, while the
+    /// order-only `||` separator is still emitted.
+    #[test]
+    fn implicit_separator_absent_when_no_implicit_deps(
+        inputs in name_list(4),
+        order_only in name_list(4),
+    ) {
+        let line = build_line(&inputs, &[], &order_only)?;
+        let expected = format!(
+            "build out: act {} || {}",
+            inputs.join(" "),
+            order_only.join(" "),
+        );
+        prop_assert_eq!(&line, &expected);
+        prop_assert!(!line.contains(" | "), "unexpected implicit separator: {}", line);
+    }
+}