diff --git a/changelog/entries/2026-07-24-router-drill-aware-vias-pad-layer-stubs.json b/changelog/entries/2026-07-24-router-drill-aware-vias-pad-layer-stubs.json
new file mode 100644
index 00000000..facac481
--- /dev/null
+++ b/changelog/entries/2026-07-24-router-drill-aware-vias-pad-layer-stubs.json
@@ -0,0 +1,10 @@
+{
+  "id": "2026-07-24-router-drill-aware-vias-pad-layer-stubs",
+  "version": "0.9.4",
+  "date": "2026-07-24",
+  "category": "fix",
+  "title": "Router vias clear drills; stubs leave pads on the pad's layer",
+  "summary": "The routing oracle now checks hole-to-hole spacing across layer spans (two vias on disjoint spans no longer collide in the drill file), probes a via barrel on every layer it spans, and can pin a connection's terminals so stubs leave a pad on a layer the pad is actually on instead of floating on an inner layer.",
+  "features": ["pcb", "autorouter", "drc"],
+  "mcpTools": ["route_nets", "run_drc", "validate_for_fab"]
+}
diff --git a/crates/vcad-ecad-pcb/examples/cm5_verdict.rs b/crates/vcad-ecad-pcb/examples/cm5_verdict.rs
index 1fadf4c4..8962732c 100644
--- a/crates/vcad-ecad-pcb/examples/cm5_verdict.rs
+++ b/crates/vcad-ecad-pcb/examples/cm5_verdict.rs
@@ -1,22 +1,80 @@
 //! Verdict driver: put the still-unrouted connections of a routed board in
 //! front of the COMPLETE window router, cluster by cluster, and demand an
-//! answer — Routed (commit-quality paths), ProvedInfeasible (bottleneck-cut
-//! certificate), or BudgetExhausted (honest unknown). The campaign's closing
-//! argument: every connection ends accounted for.
+//! answer — Routed (commit-quality paths) or ProvedInfeasible (bottleneck-cut
+//! certificate). The campaign's closing argument: every connection ends
+//! accounted for, and nothing ends "unknown".
+//!
+//! The ladder, per cluster, escalates rather than accepting an unknown:
+//!
+//! 1. **joint window, base budget** — the k connections decided together;
+//! 2. **joint window, 5× then 25× budget**, cells-per-axis raised with the last
+//!    rung so a wider search keeps its pitch at the `width + separation` floor
+//!    instead of coarsening until unrelated terminals collide in one cell;
+//! 3. **per-connection endgame** — whatever is left is decided one connection at
+//!    a time in its own window: 2 mm, then 8 mm, then 20 mm of margin, each with
+//!    a cell budget that holds the pitch at that floor. A lone connection is
+//!    settled by reachability, which is exact and cannot trip a budget: it
+//!    routes, or its severed reachable component *is* the proof.
+//!
+//! Splitting is not a fallback for weak proofs, it is what makes the
+//! certificates *per connection*: a joint infeasibility says only that the k
+//! cannot all be routed at once, so it is never charged to the individual
+//! connections — they each get their own verdict. And because each rung searches
+//! a strictly larger space than the last, the certificate that survives to the
+//! end is the strongest one available.
+//!
+//! Everything commits fail-closed through the session oracle — traces, via
+//! barrels on every layer they span, drills against the hole-to-hole rule, and
+//! diff-pair coupling scored the way the board's DRC scores it.
 //!
 //! ```bash
 //! cargo run --release -p vcad-ecad-pcb --example cm5_verdict -- routed.pcb.json [budget] [out.pcb.json] [max_cluster]
 //! ```
+//!
+//! `budget` is DFS expansions; a value below 1000 is read as a multiplier of
+//! 1e6 expansions (so `3` and `3000000` mean the same thing).
 
-use std::collections::BTreeMap;
+use std::collections::{BTreeMap, HashMap};
 use vcad_ecad_pcb::ratsnest::{compute_ratsnest, NetConnection, Netlist, NetlistNet};
-use vcad_ecad_pcb::router::complete::{route_window_complete, CompleteOutcome};
+use vcad_ecad_pcb::router::complete::{
+    route_window_complete_pinned, CompleteOutcome, TerminalLayers, ViaClass, WindowBudget,
+};
 use vcad_ecad_pcb::session::RouteSession;
 use vcad_ecad_pcb::spatial::{CopperElement, CopperGeom};
-use vcad_ir::ecad::Pcb;
+use vcad_ir::ecad::{Pcb, PcbLayer};
 use vcad_ir::Vec2;
 
-type Cluster = (Vec2, Vec2, Vec<(String, Vec2, Vec2)>);
+/// A connection awaiting a verdict.
+#[derive(Clone)]
+struct Conn {
+    net: String,
+    from: Vec2,
+    to: Vec2,
+}
+
+impl Conn {
+    fn tuple(&self) -> (String, Vec2, Vec2) {
+        (self.net.clone(), self.from, self.to)
+    }
+}
+
+/// Cluster = merged window plus the connections decided in it.
+struct Cluster {
+    lo: Vec2,
+    hi: Vec2,
+    conns: Vec<Conn>,
+}
+
+/// Joint rungs: `(budget multiplier, cells-per-axis cap)`. The cap rises with
+/// the budget — raising the window without raising the cell count would only
+/// coarsen the pitch until unrelated terminals collide.
+const JOINT_RUNGS: [(usize, usize); 3] = [(1, 48), (5, 48), (25, 96)];
+
+/// Per-connection rungs: `(window margin in mm, cells-per-axis cap)`. Each rung
+/// searches a strictly larger space than the last, so escalating can only turn
+/// an infeasibility into a routing — and the certificate that survives to the
+/// end is the strongest one (the widest space exhausted).
+const SINGLE_RUNGS: [(f64, usize); 3] = [(2.0, 160), (8.0, 320), (20.0, 640)];
 
 fn main() {
     env_logger::Builder::from_env(env_logger::Env::default().default_filter_or("info"))
@@ -25,14 +83,15 @@ fn main() {
     let mut args = std::env::args().skip(1);
     let path = args
         .next()
-        .expect("usage: cm5_verdict <routed.pcb.json> [budget]");
+        .expect("usage: cm5_verdict <routed.pcb.json> [budget] [out.pcb.json] [max_cluster]");
     let budget: usize = args
         .next()
-        .and_then(|s| s.parse().ok())
+        .and_then(|s| s.parse::<f64>().ok())
+        .map(|b| if b < 1000.0 { b * 1e6 } else { b } as usize)
         .unwrap_or(5_000_000);
     let out_json = args.next();
     let max_cluster: usize = args.next().and_then(|s| s.parse().ok()).unwrap_or(6);
-    let mut pcb: Pcb =
+    let pcb: Pcb =
         serde_json::from_str(&std::fs::read_to_string(&path).expect("read")).expect("parse");
 
     // Unrouted connections = ratsnest over the routed board.
@@ -68,180 +127,484 @@ fn main() {
     rats.retain(|l| !plane_nets.contains(l.net.as_str()));
     println!("unrouted connections (plane nets excluded): {}", rats.len());
 
-    let mut session = RouteSession::from_pcb(&pcb);
-    let layers: Vec<_> = pcb
-        .stackup
-        .layers
-        .iter()
-        .map(|l| l.layer)
-        .filter(|l| l.is_copper())
-        .collect();
-    let width = pcb.rules.default_rules.trace_width;
-    // Per-net class widths: SI-class nets must be routed and committed at
-    // their class width (the DRC's MinTraceWidth rule is per-net) — a joint
-    // path at default width would land 500+ width violations on a board
-    // whose pairs are classed at 0.2 mm.
-    let net_width: std::collections::HashMap<String, f64> = pcb
-        .rules
-        .class_rules
-        .iter()
-        .flat_map(|rule| {
-            pcb.rules
-                .net_class_assignments
-                .get(&rule.name)
-                .into_iter()
-                .flatten()
-                .map(move |net| (net.clone(), rule.trace_width))
-        })
-        .collect();
+    let clusters = cluster(&rats, max_cluster);
+    println!("clusters: {}", clusters.len());
+
+    let mut driver = Driver::new(pcb, budget);
+    for c in &clusters {
+        driver.resolve_cluster(c);
+    }
+    println!(
+        "\n== VERDICT: routed {} / proved-infeasible {} / unknown {} ==",
+        driver.routed, driver.proved, driver.unknown
+    );
+    if let Some(out) = out_json {
+        std::fs::write(&out, serde_json::to_string(&driver.pcb).expect("serialize"))
+            .expect("write");
+        eprintln!("wrote {out}");
+    }
+}
 
-    // Cluster connections whose bboxes (inflated 2mm) overlap. Two rules keep
-    // the certificates honest: a cluster never holds two connections of the
-    // same net (per-connection node-disjointness can't model same-net cell
-    // sharing), and the merged window is capped — a big coalesced window
-    // coarsens the grid pitch (MAX_AXIS_CELLS) until unrelated terminals
-    // artificially collide.
+/// Cluster connections whose bboxes (inflated 2 mm) overlap. Two rules keep the
+/// joint instances tractable: a cluster never holds two connections of the same
+/// net (per-connection node-disjointness can't model same-net cell sharing), and
+/// the merged window is capped, because the cost of a joint instance grows with
+/// its window while the *benefit* of merging does not. The cap is not what keeps
+/// the pitch honest any more — the per-rung cell budget does that, so a window
+/// stays at its `width + separation` floor however large it gets.
+fn cluster(rats: &[vcad_ecad_pcb::ratsnest::RatsnestLine], max_cluster: usize) -> Vec<Cluster> {
     const MAX_WINDOW_MM: f64 = 20.0;
     let mut clusters: Vec<Cluster> = Vec::new();
-    'c: for l in &rats {
+    'c: for l in rats {
         let (lo, hi) = (
             Vec2::new(l.from.x.min(l.to.x) - 2.0, l.from.y.min(l.to.y) - 2.0),
             Vec2::new(l.from.x.max(l.to.x) + 2.0, l.from.y.max(l.to.y) + 2.0),
         );
-        for (clo, chi, cc) in clusters.iter_mut() {
-            let merged_w = (chi.x.max(hi.x) - clo.x.min(lo.x)).abs();
-            let merged_h = (chi.y.max(hi.y) - clo.y.min(lo.y)).abs();
-            if lo.x <= chi.x
-                && clo.x <= hi.x
-                && lo.y <= chi.y
-                && clo.y <= hi.y
-                && cc.len() < max_cluster
+        let conn = Conn {
+            net: l.net.clone(),
+            from: l.from,
+            to: l.to,
+        };
+        for c in clusters.iter_mut() {
+            let merged_w = (c.hi.x.max(hi.x) - c.lo.x.min(lo.x)).abs();
+            let merged_h = (c.hi.y.max(hi.y) - c.lo.y.min(lo.y)).abs();
+            if lo.x <= c.hi.x
+                && c.lo.x <= hi.x
+                && lo.y <= c.hi.y
+                && c.lo.y <= hi.y
+                && c.conns.len() < max_cluster
                 && merged_w <= MAX_WINDOW_MM
                 && merged_h <= MAX_WINDOW_MM
-                && cc.iter().all(|(n, _, _)| n != &l.net)
+                && c.conns.iter().all(|k| k.net != conn.net)
             {
-                clo.x = clo.x.min(lo.x);
-                clo.y = clo.y.min(lo.y);
-                chi.x = chi.x.max(hi.x);
-                chi.y = chi.y.max(hi.y);
-                cc.push((l.net.clone(), l.from, l.to));
+                c.lo.x = c.lo.x.min(lo.x);
+                c.lo.y = c.lo.y.min(lo.y);
+                c.hi.x = c.hi.x.max(hi.x);
+                c.hi.y = c.hi.y.max(hi.y);
+                c.conns.push(conn);
                 continue 'c;
             }
         }
-        clusters.push((lo, hi, vec![(l.net.clone(), l.from, l.to)]));
+        clusters.push(Cluster {
+            lo,
+            hi,
+            conns: vec![conn],
+        });
     }
-    println!("clusters: {}", clusters.len());
+    clusters
+}
+
+/// Distance from `p` to the segment `a`–`b` (centreline, mm).
+fn point_on_segment(p: Vec2, a: Vec2, b: Vec2) -> f64 {
+    let (dx, dy) = (b.x - a.x, b.y - a.y);
+    let len2 = dx * dx + dy * dy;
+    let t = if len2 < 1e-18 {
+        0.0
+    } else {
+        (((p.x - a.x) * dx + (p.y - a.y) * dy) / len2).clamp(0.0, 1.0)
+    };
+    ((p.x - a.x - t * dx).powi(2) + (p.y - a.y - t * dy).powi(2)).sqrt()
+}
+
+/// Board state plus the running verdict tally.
+struct Driver {
+    pcb: Pcb,
+    session: RouteSession,
+    layers: Vec<PcbLayer>,
+    /// Per-net class trace width: SI-class nets must be searched and committed
+    /// at their class width (the DRC's MinTraceWidth rule is per-net), so a
+    /// joint path at default width would land hundreds of width violations on a
+    /// board whose pairs are classed at 0.2 mm.
+    net_width: HashMap<String, f64>,
+    default_width: f64,
+    budget: usize,
+    routed: usize,
+    proved: usize,
+    unknown: usize,
+}
 
-    let (mut routed, mut proved, mut unknown) = (0usize, 0usize, 0usize);
-    for (lo, hi, conns) in &clusters {
-        let names: Vec<&str> = conns.iter().map(|c| c.0.as_str()).collect();
-        // Search at the widest class width in the cluster (conservative:
-        // guarantees the found corridors fit every member's committed width).
-        let cluster_width = conns
+impl Driver {
+    fn new(pcb: Pcb, budget: usize) -> Self {
+        let mut session = RouteSession::from_pcb(&pcb);
+        // Judge diff-pair coupling the way the board's DRC will, pads and via
+        // annuli included. Costs a few routings; buys copper that cannot land a
+        // pair-gap violation.
+        session.set_strict_pair_coupling(true);
+        let layers: Vec<_> = pcb
+            .stackup
+            .layers
             .iter()
-            .map(|(n, _, _)| net_width.get(n).copied().unwrap_or(width))
-            .fold(width, f64::max);
-        match route_window_complete(&session, (*lo, *hi), &layers, conns, cluster_width, budget) {
-            CompleteOutcome::Routed(paths) => {
-                // Fail-closed: the window router's coarse grid can hide
-                // sub-clearance gaps its pitch cannot see, and joint paths
-                // do not know the intra-pair gap rule. Probe every segment
-                // through the (pair-aware) session before trusting the
-                // routing; a path the oracle rejects downgrades the cluster
-                // to an honest unknown.
-                // Probe-then-commit PER PATH, in order: cluster paths are
-                // node-disjoint on the coarse window grid, but the grid pitch
-                // can hide sub-clearance gaps BETWEEN two paths of the same
-                // cluster (observed: two same-cluster diagonals overlapping
-                // at 0.000mm). Probing each path against the session AFTER
-                // its clustermates committed makes mutual legality exact; a
-                // path that fails downgrades only itself to unknown.
-                let mut cluster_routed = 0usize;
-                for ((net, _, _), path) in conns.iter().zip(&paths) {
-                    let w = net_width.get(net).copied().unwrap_or(width);
-                    let legal = path.iter().all(|&(a, b, l)| {
-                        let g = vcad_ecad_pcb::spatial::CopperGeom::Segment {
-                            a,
-                            b,
-                            half_w: w / 2.0,
-                        };
-                        session.probe(&g, l, net, session.clearance_for(net)).legal
-                    });
-                    if !legal {
-                        unknown += 1;
-                        println!("UNKNOWN  [{net:?}] (path failed oracle probe)");
+            .map(|l| l.layer)
+            .filter(|l| l.is_copper())
+            .collect();
+        let net_width: HashMap<String, f64> = pcb
+            .rules
+            .class_rules
+            .iter()
+            .flat_map(|rule| {
+                pcb.rules
+                    .net_class_assignments
+                    .get(&rule.name)
+                    .into_iter()
+                    .flatten()
+                    .map(move |net| (net.clone(), rule.trace_width))
+            })
+            .collect();
+        let default_width = pcb.rules.default_rules.trace_width;
+        Self {
+            pcb,
+            session,
+            layers,
+            net_width,
+            default_width,
+            budget,
+            routed: 0,
+            proved: 0,
+            unknown: 0,
+        }
+    }
+
+    /// The copper layers each terminal of `conn` may attach on: the layers where
+    /// the net *already has copper* at that endpoint.
+    ///
+    /// A ratsnest line joins two copper groups, so an endpoint is a pad on some
+    /// layers, or a point on an existing trace or via of the net — and only
+    /// those layers are electrically live there. A stub that starts anywhere
+    /// else is dangling: nothing joins it to the group, and the board gains a
+    /// net island instead of a connection.
+    fn terminal_layers(&self, conn: &Conn) -> TerminalLayers {
+        let at = |p: Vec2| -> Vec<PcbLayer> {
+            let mut out: Vec<PcbLayer> = Vec::new();
+            for fp in &self.pcb.footprints {
+                for pad in &fp.pads {
+                    if pad.net.as_deref() != Some(conn.net.as_str()) {
                         continue;
                     }
-                    cluster_routed += 1;
-                    let w = net_width.get(net).copied().unwrap_or(width);
-                    for (a, b, layer) in path {
-                        session.commit(CopperElement {
-                            min: [a.x.min(b.x) - w, a.y.min(b.y) - w],
-                            max: [a.x.max(b.x) + w, a.y.max(b.y) + w],
-                            net: net.clone(),
-                            layer: *layer,
-                            geom: CopperGeom::Segment {
-                                a: *a,
-                                b: *b,
-                                half_w: w / 2.0,
-                            },
-                        });
-                        pcb.traces.push(vcad_ir::ecad::Trace {
-                            start: *a,
-                            end: *b,
-                            width: w,
-                            layer: *layer,
-                            net: net.clone(),
-                            source: None,
-                        });
+                    let w = vcad_ecad_pcb::geometry::pad_world_position(fp, pad);
+                    if (w.x - p.x).abs() < 1e-3 && (w.y - p.y).abs() < 1e-3 {
+                        out.extend(pad.layers.iter().filter(|l| self.layers.contains(l)));
                     }
-                    for w in path.windows(2) {
-                        let (_, b0, l0) = w[0];
-                        let (a1, _, l1) = w[1];
-                        if l0 != l1 && (b0.x - a1.x).abs() < 1e-9 && (b0.y - a1.y).abs() < 1e-9 {
-                            let r = pcb.rules.default_rules.via_diameter / 2.0;
-                            for layer in [l0, l1] {
-                                session.commit(CopperElement {
-                                    min: [b0.x - r, b0.y - r],
-                                    max: [b0.x + r, b0.y + r],
-                                    net: net.clone(),
-                                    layer,
-                                    geom: CopperGeom::Disc { center: b0, r },
-                                });
+                }
+            }
+            for trace in &self.pcb.traces {
+                if trace.net != conn.net {
+                    continue;
+                }
+                if point_on_segment(p, trace.start, trace.end) <= trace.width / 2.0 + 1e-3 {
+                    out.push(trace.layer);
+                }
+            }
+            for via in &self.pcb.vias {
+                if via.net != conn.net {
+                    continue;
+                }
+                let d = ((via.position.x - p.x).powi(2) + (via.position.y - p.y).powi(2)).sqrt();
+                if d <= via.diameter / 2.0 + 1e-3 {
+                    out.extend(self.span(via.start_layer, via.end_layer));
+                }
+            }
+            out.retain(|l| l.is_copper());
+            out.sort_by_key(|l| {
+                self.layers
+                    .iter()
+                    .position(|s| s == l)
+                    .unwrap_or(usize::MAX)
+            });
+            out.dedup();
+            out
+        };
+        TerminalLayers {
+            from: at(conn.from),
+            to: at(conn.to),
+        }
+    }
+
+    /// The via geometry this driver commits — handed to the router so its
+    /// legality model is the same one the commit will enforce.
+    fn via_class(&self) -> ViaClass {
+        ViaClass {
+            pad_diameter: self.pcb.rules.default_rules.via_diameter,
+            drill: self.pcb.rules.default_rules.via_drill,
+        }
+    }
+
+    fn width_of(&self, net: &str) -> f64 {
+        self.net_width
+            .get(net)
+            .copied()
+            .unwrap_or(self.default_width)
+    }
+
+    /// Search width for a set of connections: the widest class width among them
+    /// (conservative — the corridors found then fit every member's committed
+    /// width).
+    fn search_width(&self, conns: &[Conn]) -> f64 {
+        conns
+            .iter()
+            .map(|c| self.width_of(&c.net))
+            .fold(self.default_width, f64::max)
+    }
+
+    fn resolve_cluster(&mut self, cluster: &Cluster) {
+        let names: Vec<&str> = cluster.conns.iter().map(|c| c.net.as_str()).collect();
+        let mut pending = cluster.conns.clone();
+        // Joint rungs only earn their keep when there is something joint to
+        // decide; a lone connection goes straight to the exact endgame.
+        if pending.len() > 1 {
+            let width = self.search_width(&pending);
+            for (mul, cells) in JOINT_RUNGS {
+                let limits =
+                    WindowBudget::new(self.budget.saturating_mul(mul)).with_max_axis_cells(cells);
+                let conns: Vec<(String, Vec2, Vec2)> = pending.iter().map(|c| c.tuple()).collect();
+                let pins: Vec<TerminalLayers> =
+                    pending.iter().map(|c| self.terminal_layers(c)).collect();
+                match route_window_complete_pinned(
+                    &self.session,
+                    (cluster.lo, cluster.hi),
+                    &self.layers,
+                    &conns,
+                    &pins,
+                    width,
+                    Some(self.via_class()),
+                    limits,
+                ) {
+                    CompleteOutcome::Routed(paths) => {
+                        // Probe-then-commit PER PATH, in order: cluster paths
+                        // are node-disjoint on the window grid, but the pitch
+                        // can hide sub-clearance gaps BETWEEN two paths of the
+                        // same cluster. Probing each path against the session
+                        // AFTER its clustermates committed makes mutual
+                        // legality exact; a path the oracle rejects drops to
+                        // the per-connection endgame rather than to an unknown.
+                        let mut rejected = Vec::new();
+                        let mut committed = 0usize;
+                        for (conn, path) in pending.iter().zip(&paths) {
+                            if self.commit_if_legal(conn, path) {
+                                committed += 1;
+                                self.routed += 1;
+                            } else {
+                                rejected.push(conn.clone());
                             }
-                            pcb.vias.push(vcad_ir::ecad::Via {
-                                position: b0,
-                                diameter: pcb.rules.default_rules.via_diameter,
-                                drill: pcb.rules.default_rules.via_drill,
-                                start_layer: l0,
-                                end_layer: l1,
-                                net: net.clone(),
-                                source: None,
-                            });
                         }
+                        if committed > 0 {
+                            println!(
+                                "ROUTED   {names:?} ({committed}/{} committed jointly at \
+                                 {mul}x budget)",
+                                pending.len()
+                            );
+                        }
+                        pending = rejected;
+                        break;
+                    }
+                    CompleteOutcome::ProvedInfeasible { reason } => {
+                        // A joint proof is NOT a per-connection proof: it says
+                        // the k cannot all be routed at once. Charge it to
+                        // nobody and let each connection earn its own verdict.
+                        println!("JOINT-NO {names:?}: {reason}");
+                        break;
+                    }
+                    CompleteOutcome::BudgetExhausted => continue,
+                }
+            }
+        }
+        for conn in std::mem::take(&mut pending) {
+            self.resolve_single(&conn);
+        }
+    }
+
+    /// Decide one connection on its own. Reachability is exact for k = 1, so
+    /// every rung answers definitively; escalation exists to make a *routing*
+    /// more likely (wider window, finer pitch) and, failing that, to make the
+    /// surviving certificate the strongest one available.
+    fn resolve_single(&mut self, conn: &Conn) {
+        let width = self.width_of(&conn.net);
+        let mut last: Option<(bool, String)> = None;
+        for (margin, cells) in SINGLE_RUNGS {
+            let window = (
+                Vec2::new(
+                    conn.from.x.min(conn.to.x) - margin,
+                    conn.from.y.min(conn.to.y) - margin,
+                ),
+                Vec2::new(
+                    conn.from.x.max(conn.to.x) + margin,
+                    conn.from.y.max(conn.to.y) + margin,
+                ),
+            );
+            match route_window_complete_pinned(
+                &self.session,
+                window,
+                &self.layers,
+                &[conn.tuple()],
+                &[self.terminal_layers(conn)],
+                width,
+                Some(self.via_class()),
+                WindowBudget::new(self.budget).with_max_axis_cells(cells),
+            ) {
+                CompleteOutcome::Routed(paths) => {
+                    if self.commit_if_legal(conn, &paths[0]) {
+                        self.routed += 1;
+                        println!("ROUTED   [{:?}] (alone, {margin:.0}mm window)", conn.net);
+                        return;
                     }
+                    last = Some((
+                        false,
+                        format!(
+                            "window path rejected by the fail-closed session oracle \
+                             ({margin:.0}mm window, {cells} cells/axis)"
+                        ),
+                    ));
                 }
-                routed += cluster_routed;
-                if cluster_routed > 0 {
-                    println!(
-                        "ROUTED   {names:?} ({cluster_routed}/{} committed)",
-                        conns.len()
-                    );
+                CompleteOutcome::ProvedInfeasible { reason } => last = Some((true, reason)),
+                // k = 1 is decided by reachability, which cannot trip the
+                // expansion budget — but keep the honest branch anyway.
+                CompleteOutcome::BudgetExhausted => {
+                    last = Some((
+                        false,
+                        format!("budget {} exhausted ({margin:.0}mm window)", self.budget),
+                    ))
                 }
             }
-            CompleteOutcome::ProvedInfeasible { reason } => {
-                proved += conns.len();
-                println!("PROVED   {names:?}: {reason}");
+        }
+        match last {
+            Some((true, reason)) => {
+                self.proved += 1;
+                println!("PROVED   [{:?}]: {reason}", conn.net);
+            }
+            Some((false, why)) => {
+                self.unknown += 1;
+                println!("UNKNOWN  [{:?}] ({why})", conn.net);
             }
-            CompleteOutcome::BudgetExhausted => {
-                unknown += conns.len();
-                println!("UNKNOWN  {names:?} (budget {budget} exhausted)");
+            None => {
+                self.unknown += 1;
+                println!("UNKNOWN  [{:?}] (no rung reported)", conn.net);
             }
         }
     }
-    println!("\n== VERDICT: routed {routed} / proved-infeasible {proved} / unknown {unknown} ==");
-    if let Some(out) = out_json {
-        std::fs::write(&out, serde_json::to_string(&pcb).expect("serialize")).expect("write");
-        eprintln!("wrote {out}");
+
+    /// Every copper layer a via spanning `a`..`b` passes through, in stack
+    /// order. A barrel's annulus lands on all of them, so all of them must
+    /// clear.
+    fn span(&self, a: PcbLayer, b: PcbLayer) -> Vec<PcbLayer> {
+        let idx = |l: PcbLayer| self.layers.iter().position(|s| *s == l).unwrap_or(0);
+        let (i, j) = (idx(a), idx(b));
+        self.layers[i.min(j)..=i.max(j)].to_vec()
+    }
+
+    /// Probe a candidate path — segments *and* the vias as they will be
+    /// committed — against the session, and commit it only if every piece is
+    /// legal. Returns whether the path landed on the board.
+    fn commit_if_legal(&mut self, conn: &Conn, path: &[(Vec2, Vec2, PcbLayer)]) -> bool {
+        let net = &conn.net;
+        let w = self.width_of(net);
+        let clr = self.session.clearance_for(net);
+        let via_d = self.pcb.rules.default_rules.via_diameter;
+        let via_r = via_d / 2.0;
+        let segs_ok = path.iter().all(|&(a, b, layer)| {
+            self.session
+                .probe(
+                    &CopperGeom::Segment {
+                        a,
+                        b,
+                        half_w: w / 2.0,
+                    },
+                    layer,
+                    net,
+                    clr,
+                )
+                .legal
+        });
+        if !segs_ok {
+            return false;
+        }
+        // Layer transitions become real vias, so they must clear as real vias:
+        // probing only the traces let via copper land unchecked. Consecutive
+        // transitions at one point are ONE barrel spanning the whole run —
+        // emitting them as separate vias would stack drills at zero spacing and
+        // fail hole-to-hole against itself.
+        let mut vias: Vec<(Vec2, PcbLayer, PcbLayer)> = Vec::new();
+        for w in path.windows(2) {
+            let (_, b0, l0) = w[0];
+            let (a1, _, l1) = w[1];
+            if l0 == l1 || (b0.x - a1.x).abs() > 1e-9 || (b0.y - a1.y).abs() > 1e-9 {
+                continue;
+            }
+            match vias.last_mut() {
+                Some((p, _, end))
+                    if (p.x - b0.x).abs() < 1e-9 && (p.y - b0.y).abs() < 1e-9 && *end == l0 =>
+                {
+                    *end = l1;
+                }
+                _ => vias.push((b0, l0, l1)),
+            }
+        }
+        let via_drill = self.pcb.rules.default_rules.via_drill;
+        let vias_ok = vias.iter().all(|&(p, l0, l1)| {
+            // The barrel exists on every layer it spans, not just its two ends.
+            self.span(l0, l1).iter().all(|&layer| {
+                self.session
+                    .probe(&CopperGeom::Disc { center: p, r: via_r }, layer, net, clr)
+                    .legal
+            })
+            // Hole-to-hole is layer- and net-agnostic, so the copper probe
+            // above cannot see it: two vias on disjoint layer spans share no
+            // layer yet still collide in the drill file.
+            && self.session.probe_drill(p, via_drill).legal
+            // ...and two vias of THIS path must clear each other, which the
+            // session cannot judge until they are committed.
+            && vias.iter().all(|&(q, _, _)| {
+                let d = ((q.x - p.x).powi(2) + (q.y - p.y).powi(2)).sqrt() - via_drill;
+                (q.x - p.x).abs() + (q.y - p.y).abs() < 1e-9
+                    || d >= self.pcb.rules.hole_to_hole - 1e-6
+            })
+        });
+        if !vias_ok {
+            return false;
+        }
+        for &(a, b, layer) in path {
+            self.session.commit(CopperElement {
+                min: [a.x.min(b.x) - w, a.y.min(b.y) - w],
+                max: [a.x.max(b.x) + w, a.y.max(b.y) + w],
+                net: net.clone(),
+                layer,
+                geom: CopperGeom::Segment {
+                    a,
+                    b,
+                    half_w: w / 2.0,
+                },
+            });
+            self.pcb.traces.push(vcad_ir::ecad::Trace {
+                start: a,
+                end: b,
+                width: w,
+                layer,
+                net: net.clone(),
+                source: None,
+            });
+        }
+        for (p, l0, l1) in vias {
+            for layer in self.span(l0, l1) {
+                self.session.commit(CopperElement {
+                    min: [p.x - via_r, p.y - via_r],
+                    max: [p.x + via_r, p.y + via_r],
+                    net: net.clone(),
+                    layer,
+                    geom: CopperGeom::Disc {
+                        center: p,
+                        r: via_r,
+                    },
+                });
+            }
+            self.session.commit_drill(p, via_drill);
+            self.pcb.vias.push(vcad_ir::ecad::Via {
+                position: p,
+                diameter: via_d,
+                drill: via_drill,
+                start_layer: l0,
+                end_layer: l1,
+                net: net.clone(),
+                source: None,
+            });
+        }
+        true
     }
 }
diff --git a/crates/vcad-ecad-pcb/src/router/complete.rs b/crates/vcad-ecad-pcb/src/router/complete.rs
index da58368b..fb3a3adb 100644
--- a/crates/vcad-ecad-pcb/src/router/complete.rs
+++ b/crates/vcad-ecad-pcb/src/router/complete.rs
@@ -78,7 +78,7 @@
 //! search (it ignores which net must pair with which terminal), so it can
 //! only fire on genuinely infeasible instances.
 
-use std::collections::{HashMap, HashSet, VecDeque};
+use std::collections::{BTreeMap, HashMap, HashSet, VecDeque};
 
 use vcad_ir::ecad::PcbLayer;
 use vcad_ir::Vec2;
@@ -86,9 +86,78 @@ use vcad_ir::Vec2;
 use crate::session::RouteSession;
 use crate::spatial::CopperGeom;
 
-/// Hard cap on grid cells per axis; the pitch coarsens to fit. Keeps the
+/// Default cap on grid cells per axis; the pitch coarsens to fit. Keeps the
 /// state space honest (≤ 48×48×4 ≈ 9.2k nodes).
-const MAX_AXIS_CELLS: usize = 48;
+pub const MAX_AXIS_CELLS: usize = 48;
+
+/// Which copper layers a connection's two terminals may attach on — normally
+/// the layers each terminal's pad actually exists on.
+///
+/// Without this the search takes the first layer whose cell happens to be free,
+/// which on a ten-layer board is usually *not* the pad's layer: the emitted stub
+/// then floats on an inner layer with nothing joining it to the pad, and the
+/// board grows a net island instead of a connection. Empty means unconstrained
+/// (the whole searched stack).
+#[derive(Debug, Clone, Default)]
+pub struct TerminalLayers {
+    /// Layers the `from` terminal may attach on.
+    pub from: Vec<PcbLayer>,
+    /// Layers the `to` terminal may attach on.
+    pub to: Vec<PcbLayer>,
+}
+
+/// The via the caller will actually commit for a layer change.
+///
+/// Supplying it makes the router's legality model identical to the caller's
+/// commit rule instead of merely similar: the barrel is probed at its real pad
+/// size, the drill is checked against the board's hole-to-hole rule (which no
+/// layer-scoped copper probe can see), and the grid pitch is floored so two
+/// vias of one routing can never land closer than that rule allows. Without it
+/// the router falls back to a pad-size heuristic and leaves drills to the
+/// caller — which is where a "routed" path can still fail a fail-closed commit.
+#[derive(Debug, Clone, Copy)]
+pub struct ViaClass {
+    /// Via pad (annulus) diameter, mm.
+    pub pad_diameter: f64,
+    /// Drilled hole diameter, mm.
+    pub drill: f64,
+}
+
+/// Search resources the caller may raise without weakening the decision
+/// procedure: the DFS expansion budget and the grid's cells-per-axis cap.
+///
+/// The two are coupled on purpose. A wide window at a fixed cell cap coarsens
+/// the pitch until unrelated terminals collide in one cell and free channels
+/// vanish — the discretization, not the copper, then decides the verdict.
+/// Raising [`Self::max_axis_cells`] alongside the window keeps the pitch at its
+/// `(width + separation)` floor, so the answer stays about the board.
+#[derive(Debug, Clone, Copy)]
+pub struct WindowBudget {
+    /// Maximum DFS node expansions before the search reports "unknown".
+    pub expansions: usize,
+    /// Cap on grid cells per axis. The pitch never goes *below* the
+    /// `width + separation` floor, so a generous cap simply stops the pitch
+    /// from coarsening on a large window.
+    pub max_axis_cells: usize,
+}
+
+impl WindowBudget {
+    /// `expansions` at the default cell cap.
+    pub fn new(expansions: usize) -> Self {
+        Self {
+            expansions,
+            max_axis_cells: MAX_AXIS_CELLS,
+        }
+    }
+
+    /// Same budget with a raised cells-per-axis cap.
+    pub fn with_max_axis_cells(self, max_axis_cells: usize) -> Self {
+        Self {
+            max_axis_cells,
+            ..self
+        }
+    }
+}
 
 /// Outcome of the complete window router.
 #[derive(Debug, Clone)]
@@ -129,6 +198,45 @@ pub fn route_window_complete(
     width: f64,
     budget: usize,
 ) -> CompleteOutcome {
+    route_window_complete_with(
+        session,
+        window,
+        layers,
+        conns,
+        width,
+        WindowBudget::new(budget),
+    )
+}
+
+/// [`route_window_complete`] with explicit search resources — see
+/// [`WindowBudget`].
+pub fn route_window_complete_with(
+    session: &RouteSession,
+    window: (Vec2, Vec2),
+    layers: &[PcbLayer],
+    conns: &[(String, Vec2, Vec2)],
+    width: f64,
+    limits: WindowBudget,
+) -> CompleteOutcome {
+    route_window_complete_pinned(session, window, layers, conns, &[], width, None, limits)
+}
+
+/// [`route_window_complete_with`], with each connection's terminals pinned to
+/// the layers they may attach on (see [`TerminalLayers`]) and the caller's real
+/// via geometry (see [`ViaClass`]). A shorter `terminals` slice than `conns`
+/// leaves the remaining connections unconstrained.
+#[allow(clippy::too_many_arguments)]
+pub fn route_window_complete_pinned(
+    session: &RouteSession,
+    window: (Vec2, Vec2),
+    layers: &[PcbLayer],
+    conns: &[(String, Vec2, Vec2)],
+    terminals: &[TerminalLayers],
+    width: f64,
+    via: Option<ViaClass>,
+    limits: WindowBudget,
+) -> CompleteOutcome {
+    let budget = limits.expansions;
     if conns.is_empty() {
         return CompleteOutcome::Routed(Vec::new());
     }
@@ -143,16 +251,48 @@ pub fn route_window_complete(
         .map(|(n, _, _)| session.clearance_for(n))
         .collect();
     let max_clearance = clearances.iter().cloned().fold(0.0_f64, f64::max);
-    let grid = WinGrid::new(window, width, max_clearance);
+    // Pair-aware pitch. Node disjointness is only a *sufficient* legality rule
+    // when one pitch of separation satisfies every rule that can apply between
+    // two paths — and between the two legs of a declared differential pair the
+    // probe demands the intra-pair GAP, which routinely exceeds the base
+    // clearance. Two twins in one window at clearance pitch route uncoupled and
+    // then fail the oracle (the fail-closed probe the caller commits through),
+    // which shows up as an honest-but-avoidable unknown. Spacing the grid by the
+    // widest gap among the window's twin pairs restores "distinct cells ⇒
+    // mutually legal" for pairs, exactly as it already holds for singles.
+    let mut separation = max_clearance;
+    for (i, (a, _, _)) in conns.iter().enumerate() {
+        for (b, _, _) in conns.iter().skip(i + 1) {
+            if let Some(gap) = session.pair_gap_between(a, b) {
+                separation = separation.max(gap);
+            }
+        }
+    }
+    // Second pitch floor: two vias one cell apart must satisfy the board's
+    // hole-to-hole rule, or a routing this model calls legal lands drill
+    // collisions the moment it is committed.
+    let drill_floor = via.map_or(0.0, |v| v.drill + session.hole_to_hole());
+    let grid = WinGrid::new(
+        window,
+        width,
+        separation,
+        drill_floor,
+        limits.max_axis_cells,
+    );
     let plane = grid.nx * grid.ny;
     let nl = layers.len();
     let n_nodes = plane * nl;
     let half_w = width / 2.0;
-    // Via legality is probed as a disc covering the real microvia pad (the
-    // largest via class this router ever realizes is the adjacent-layer
-    // microvia) on both spanned layers. Probing smaller than the committed
-    // pad let verdict copper pass here and fail board DRC by the difference.
-    let via_r = (width * 1.5).max(0.11);
+    // Via legality is probed as a disc covering the real committed pad on every
+    // spanned layer. Probing smaller than the committed pad let verdict copper
+    // pass here and fail board DRC by the difference.
+    let via_r = (width * 1.5)
+        .max(0.11)
+        .max(via.map_or(0.0, |v| v.pad_diameter / 2.0));
+    let via_drill = via.map(|v| v.drill);
+    // Every layer change the router emits must also clear existing *holes*.
+    let barrel_ok =
+        |center: Vec2| -> bool { via_drill.is_none_or(|d| session.probe_drill(center, d).legal) };
 
     // --- Free-node raster (fixed copper only) ----------------------------
     // A node is free iff a zero-length capsule (trace centre) at the cell
@@ -184,35 +324,137 @@ pub fn route_window_complete(
     // determinism; the connector from the exact endpoint to the cell centre
     // must itself probe legal.
     let mut terms: Vec<(usize, usize)> = Vec::with_capacity(conns.len()); // (src node, dst node)
+    /// Per-connection escape layers: `Some(pad layer)` when that terminal
+    /// reaches the grid through a stub-plus-via dog-bone rather than landing on
+    /// the pad's own layer.
+    type Escape = (Option<PcbLayer>, Option<PcbLayer>);
+    let mut escapes: Vec<Escape> = Vec::with_capacity(conns.len());
     for (ci, (net, from, to)) in conns.iter().enumerate() {
         let clr = clearances[ci];
-        let attach = |p: Vec2| -> Option<usize> {
-            let cell = grid.snap(p);
-            let c = grid.world(cell);
-            (0..nl).find_map(|li| {
-                let node = li * plane + cell;
-                let conn_ok = session
-                    .probe(
-                        &CopperGeom::Segment { a: p, b: c, half_w },
-                        layers[li],
-                        net,
-                        clr,
-                    )
-                    .legal;
-                (free[node] && conn_ok).then_some(node)
+        let pinned = terminals.get(ci);
+        // Attachment candidates: cells in rings around the snapped one, nearest
+        // first. A pad on a fine-pitch part often has its own nearest cell
+        // centre buried in a neighbour's clearance while a cell one step out is
+        // free; since the pad-to-cell connector is probed exactly either way,
+        // reaching for that cell is not a cheat — and it is what lets the stub
+        // stay on the pad's own layer instead of surfacing on an inner one with
+        // nothing joining it to the pad.
+        // Reach measured in millimetres, not cells: a dog-bone escape lands
+        // within about a millimetre of its pad whatever the pitch happens to be.
+        let attach_ring = ((1.0 / grid.pitch).ceil() as i64).clamp(2, 4);
+        let attach = |p: Vec2, allowed: &[PcbLayer]| -> Option<(usize, Option<PcbLayer>)> {
+            let base = grid.snap(p);
+            let (bx, by) = ((base % grid.nx) as i64, (base / grid.nx) as i64);
+            let mut cands: Vec<(i64, usize)> = Vec::new();
+            for dy in -attach_ring..=attach_ring {
+                for dx in -attach_ring..=attach_ring {
+                    let (x, y) = (bx + dx, by + dy);
+                    if x < 0 || y < 0 || x >= grid.nx as i64 || y >= grid.ny as i64 {
+                        continue;
+                    }
+                    cands.push((dx * dx + dy * dy, y as usize * grid.nx + x as usize));
+                }
+            }
+            cands.sort_unstable();
+            let stub_ok = |p: Vec2, c: Vec2, layer: PcbLayer| {
+                session
+                    .probe(&CopperGeom::Segment { a: p, b: c, half_w }, layer, net, clr)
+                    .legal
+            };
+            // First choice: land directly on a layer the pad is on. Nothing to
+            // join, nothing to drill.
+            let direct = cands.iter().find_map(|&(_, cell)| {
+                let c = grid.world(cell);
+                (0..nl)
+                    .filter(|&li| allowed.is_empty() || allowed.contains(&layers[li]))
+                    .find_map(|li| {
+                        (free[li * plane + cell] && stub_ok(p, c, layers[li]))
+                            .then_some((li * plane + cell, None))
+                    })
+            });
+            if direct.is_some() || allowed.is_empty() {
+                return direct;
+            }
+            // Otherwise escape like a real router does: a stub on the pad's own
+            // layer to a nearby cell, then a via down to the layer the search
+            // wants. The whole barrel is probed — pad copper on every layer it
+            // spans plus the hole-to-hole rule — so the escape is legal by the
+            // same oracle that will judge the committed board, not by assumption.
+            cands.iter().find_map(|&(_, cell)| {
+                let c = grid.world(cell);
+                if dist(p, c) < 1e-6 {
+                    // Pad centre on the cell centre leaves no stub to carry the
+                    // layer change; take another cell.
+                    return None;
+                }
+                let pad_li = (0..nl).find(|&li| allowed.contains(&layers[li]))?;
+                if !stub_ok(p, c, layers[pad_li]) || !barrel_ok(c) {
+                    return None;
+                }
+                (0..nl).find_map(|li| {
+                    if li == pad_li || !free[li * plane + cell] {
+                        return None;
+                    }
+                    let span = if li < pad_li {
+                        li..=pad_li
+                    } else {
+                        pad_li..=li
+                    };
+                    let barrel = CopperGeom::Disc {
+                        center: c,
+                        r: via_r,
+                    };
+                    span.clone()
+                        .all(|s| session.probe(&barrel, layers[s], net, clr).legal)
+                        .then_some((li * plane + cell, Some(layers[pad_li])))
+                })
             })
         };
-        match (attach(*from), attach(*to)) {
-            (Some(s), Some(t)) => terms.push((s, t)),
-            _ => {
+        let (from_pins, to_pins) = pinned
+            .map(|t| (t.from.as_slice(), t.to.as_slice()))
+            .unwrap_or((&[], &[]));
+        match (attach(*from, from_pins), attach(*to, to_pins)) {
+            (Some((s, se)), Some((t, te))) => {
+                terms.push((s, t));
+                escapes.push((se, te));
+            }
+            (s, _) => {
+                // Name the copper that walls the pad in: the cut here is the
+                // ring of blockers around the terminal itself.
+                let stuck = if s.is_none() { *from } else { *to };
+                let pins = if s.is_none() { from_pins } else { to_pins };
+                let on = if pins.is_empty() {
+                    format!("all {nl} copper layers")
+                } else {
+                    format!("its {} pad layer(s) {pins:?}", pins.len())
+                };
+                let census = blocking_nets(
+                    session,
+                    &CopperGeom::Segment {
+                        a: stuck,
+                        b: grid.world(grid.snap(stuck)),
+                        half_w,
+                    },
+                    layers,
+                    net,
+                    clr,
+                );
                 return CompleteOutcome::ProvedInfeasible {
                     reason: format!(
                         "terminal of net {net} at ({:.2}, {:.2})/({:.2}, {:.2}) has no \
-                         clearance-legal grid attachment on any layer — the pad is walled \
-                         in at the current rules and grid pitch {:.3} mm",
-                        from.x, from.y, to.x, to.y, grid.pitch
+                         clearance-legal grid attachment — the pad at ({:.2}, {:.2}) is \
+                         walled in on {on} by {} at the current rules and grid pitch \
+                         {:.3} mm",
+                        from.x,
+                        from.y,
+                        to.x,
+                        to.y,
+                        stuck.x,
+                        stuck.y,
+                        name_census(&census),
+                        grid.pitch
                     ),
-                }
+                };
             }
         }
     }
@@ -220,16 +462,19 @@ pub fn route_window_complete(
     // node-disjoint — a genuine infeasibility at this pitch. Two connections
     // of the SAME net sharing a cell is not: same-net copper may legally
     // share space, but this model's per-connection node-disjointness can't
-    // express that, so the honest answer is unknown, never a proof.
+    // express that, so the honest answer is unknown, never a proof. A single
+    // connection whose OWN two terminals snap into one cell is neither: it is
+    // simply shorter than the pitch, and its path is that one node.
     {
-        let mut seen: HashMap<usize, &str> = HashMap::new();
+        let mut seen: HashMap<usize, (&str, usize)> = HashMap::new();
         for (ci, &(s, t)) in terms.iter().enumerate() {
             for node in [s, t] {
                 match seen.get(&node) {
                     None => {
-                        seen.insert(node, conns[ci].0.as_str());
+                        seen.insert(node, (conns[ci].0.as_str(), ci));
                     }
-                    Some(&other) if other != conns[ci].0 => {
+                    Some(&(_, cj)) if cj == ci => {}
+                    Some(&(other, _)) if other != conns[ci].0 => {
                         return CompleteOutcome::ProvedInfeasible {
                             reason: format!(
                                 "terminals of nets {} and {other} collide in the same \
@@ -244,6 +489,32 @@ pub fn route_window_complete(
             }
         }
     }
+    // An escape barrel occupies its cell on every layer it spans, so those
+    // nodes are no longer free for anyone. Terminal nodes are exempt: they are
+    // already reserved one-per-connection by node disjointness, and blanking
+    // one here would make its own connection unroutable.
+    {
+        let terminal: HashSet<usize> = terms.iter().flat_map(|&(s, t)| [s, t]).collect();
+        for (ci, &(se, te)) in escapes.iter().enumerate() {
+            for (escape, node) in [(se, terms[ci].0), (te, terms[ci].1)] {
+                let Some(pad_layer) = escape else { continue };
+                let (cell, attach_li) = (node % plane, node / plane);
+                let pad_li = layers.iter().position(|l| *l == pad_layer).unwrap_or(0);
+                let span = if attach_li < pad_li {
+                    attach_li..=pad_li
+                } else {
+                    pad_li..=attach_li
+                };
+                for li in span {
+                    let barrel_node = li * plane + cell;
+                    if !terminal.contains(&barrel_node) {
+                        free[barrel_node] = false;
+                    }
+                }
+            }
+        }
+    }
+    let free = free;
 
     // --- Edge legality (lazy, memoized) ----------------------------------
     let mut edge_memo: HashMap<u64, bool> = HashMap::new();
@@ -278,10 +549,11 @@ pub fn route_window_complete(
                 center: grid.world(ca),
                 r: via_r,
             };
-            conns.iter().zip(&clearances).all(|((net, _, _), &clr)| {
-                session.probe(&disc, layers[la], net, clr).legal
-                    && session.probe(&disc, layers[lb], net, clr).legal
-            })
+            barrel_ok(grid.world(ca))
+                && conns.iter().zip(&clearances).all(|((net, _, _), &clr)| {
+                    session.probe(&disc, layers[la], net, clr).legal
+                        && session.probe(&disc, layers[lb], net, clr).legal
+                })
         };
         edge_memo.insert(key, ok);
         ok
@@ -313,6 +585,58 @@ pub fn route_window_complete(
         out
     };
 
+    // --- One connection: reachability decides it exactly ------------------
+    // With k = 1 there is nothing to be node-disjoint *from*, so "a joint
+    // routing exists" collapses to s–t reachability over the free graph. BFS
+    // settles that in O(E): either a shortest path (fewest cells, hence least
+    // copper) or an exhausted reachable component, which *is* the proof. No
+    // budget can trip, so a lone connection never comes back unknown — the
+    // exhaustive DFS is only ever needed to decide genuinely joint instances.
+    if conns.len() == 1 {
+        let (s, t) = terms[0];
+        let empty = BitSet::new(n_nodes);
+        return match bfs_path(s, t, &free, &empty, &neighbors, &mut edge_ok) {
+            Ok(path) => CompleteOutcome::Routed(vec![emit_segments(
+                &grid, plane, layers, conns[0].1, conns[0].2, escapes[0], &path,
+            )]),
+            Err(reached_from) => {
+                // Report the tighter pocket. The graph is undirected, so either
+                // terminal's reachable component certifies the severance; the
+                // one enclosed by fewer nodes names a small, checkable cut
+                // instead of "everything but this corner".
+                let reached_to = bfs_path(t, usize::MAX, &free, &empty, &neighbors, &mut edge_ok)
+                    .err()
+                    .unwrap_or_default();
+                let live = |r: &Vec<bool>| r.iter().filter(|v| **v).count();
+                let (reached, from_side) =
+                    if live(&reached_to) > 0 && live(&reached_to) < live(&reached_from) {
+                        (reached_to, false)
+                    } else {
+                        (reached_from, true)
+                    };
+                CompleteOutcome::ProvedInfeasible {
+                    reason: severed_reason(
+                        session,
+                        &grid,
+                        &Topology {
+                            plane,
+                            layers,
+                            via_r,
+                            half_w,
+                        },
+                        &conns[0],
+                        clearances[0],
+                        &free,
+                        &reached,
+                        &neighbors,
+                        terms[0],
+                        from_side,
+                    ),
+                }
+            }
+        };
+    }
+
     // --- Max-flow necessary-condition pre-pass ---------------------------
     let (flow, cut_cells) = max_node_disjoint_flow(&free, plane, grid.nx, nl, &terms, &neighbors);
     if flow < conns.len() {
@@ -347,10 +671,85 @@ pub fn route_window_complete(
                 lo.y - grid.pitch / 2.0,
                 hi.y + grid.pitch / 2.0,
             ));
+        } else {
+            // Flow 0 with an empty min *vertex* cut means the terminals are
+            // outright severed: nothing is saturated, so the cut is the ring of
+            // blocked nodes enclosing the sources. Name it — a certificate that
+            // does not say where the wall is, or whose copper it is, is not
+            // much of a certificate.
+            let mut reached = vec![false; n_nodes];
+            for &(s, _) in &terms {
+                if !free[s] || reached[s] {
+                    continue;
+                }
+                if let Err(seen) = bfs_path(
+                    s,
+                    usize::MAX,
+                    &free,
+                    &BitSet::new(n_nodes),
+                    &neighbors,
+                    &mut edge_ok,
+                ) {
+                    for (v, r) in seen.iter().enumerate() {
+                        reached[v] |= *r;
+                    }
+                }
+            }
+            reason.push_str(&format!(
+                " ({})",
+                frontier_census(
+                    session,
+                    &grid,
+                    &Topology {
+                        plane,
+                        layers,
+                        via_r,
+                        half_w,
+                    },
+                    &conns[0].0,
+                    clearances[0],
+                    &free,
+                    &reached,
+                    &neighbors,
+                )
+            ));
         }
         return CompleteOutcome::ProvedInfeasible { reason };
     }
 
+    // --- Cheap witness attempt: sequential shortest paths ------------------
+    // The DFS's first descent is a greedy *walk*, not a shortest path, so on a
+    // wide window it can wander for millions of expansions before its first
+    // completion — the dominant source of honest-but-avoidable unknowns. A few
+    // sequential BFS assignments (each net taking a shortest path through what
+    // the earlier nets left free) find the easy joint routings in milliseconds.
+    // Success is a witness: the paths are node-disjoint by construction, so it
+    // needs no proof. Failure proves nothing and falls through to the
+    // exhaustive search, so completeness is untouched.
+    for order in attempt_orders(&terms, grid.nx, plane) {
+        if let Some(paths) =
+            sequential_bfs(&order, &terms, &free, n_nodes, &neighbors, &mut edge_ok)
+        {
+            return CompleteOutcome::Routed(
+                paths
+                    .iter()
+                    .enumerate()
+                    .map(|(ci, path)| {
+                        emit_segments(
+                            &grid,
+                            plane,
+                            layers,
+                            conns[ci].1,
+                            conns[ci].2,
+                            escapes[ci],
+                            path,
+                        )
+                    })
+                    .collect(),
+            );
+        }
+    }
+
     // --- Exhaustive backtracking DFS -------------------------------------
     let mut search = Search {
         free: &free,
@@ -376,6 +775,7 @@ pub fn route_window_complete(
                     layers,
                     conns[ci].1,
                     conns[ci].2,
+                    escapes[ci],
                     path,
                 ));
             }
@@ -521,13 +921,24 @@ fn emit_segments(
     layers: &[PcbLayer],
     from: Vec2,
     to: Vec2,
+    escape: (Option<PcbLayer>, Option<PcbLayer>),
     path: &[usize],
 ) -> Vec<(Vec2, Vec2, PcbLayer)> {
     let mut segs: Vec<(Vec2, Vec2, PcbLayer)> = Vec::new();
     if path.is_empty() {
         return segs;
     }
-    let mut run: Vec<Vec2> = vec![from];
+    // A dog-bone terminal contributes its stub on the pad's own layer; the
+    // layer change at the stub's far end is a via the caller materializes from
+    // the layer discontinuity, exactly as for a mid-path layer change.
+    let first_cell = grid.world(path[0] % plane);
+    let mut run: Vec<Vec2> = match escape.0 {
+        Some(pad_layer) => {
+            segs.push((from, first_cell, pad_layer));
+            vec![first_cell]
+        }
+        None => vec![from],
+    };
     let mut run_layer = path[0] / plane;
     let flush = |run: &mut Vec<Vec2>, layer: PcbLayer, segs: &mut Vec<(Vec2, Vec2, PcbLayer)>| {
         let pts = simplify(run);
@@ -555,13 +966,302 @@ fn emit_segments(
             run.push(w);
         }
     }
-    if run.last().map(|p| dist(*p, to) > 1e-9).unwrap_or(true) {
-        run.push(to);
+    match escape.1 {
+        Some(pad_layer) => {
+            let last_cell = grid.world(path[path.len() - 1] % plane);
+            flush(&mut run, layers[run_layer], &mut segs);
+            segs.push((last_cell, to, pad_layer));
+        }
+        None => {
+            if run.last().map(|p| dist(*p, to) > 1e-9).unwrap_or(true) {
+                run.push(to);
+            }
+            flush(&mut run, layers[run_layer], &mut segs);
+        }
     }
-    flush(&mut run, layers[run_layer], &mut segs);
     segs
 }
 
+/// The window discretization facts the path and certificate helpers share.
+struct Topology<'a> {
+    plane: usize,
+    layers: &'a [PcbLayer],
+    via_r: f64,
+    half_w: f64,
+}
+
+/// Shortest path (fewest nodes) from `start` to `goal` over free, unoccupied
+/// nodes joined by legal edges.
+///
+/// On failure the reachable set is returned — the exhausted component that *is*
+/// the infeasibility proof for a single connection. Passing `usize::MAX` as
+/// `goal` asks for that set outright.
+fn bfs_path(
+    start: usize,
+    goal: usize,
+    free: &[bool],
+    occ: &BitSet,
+    neighbors: &dyn Fn(usize) -> Vec<usize>,
+    edge_ok: &mut dyn FnMut(usize, usize) -> bool,
+) -> Result<Vec<usize>, Vec<bool>> {
+    let mut seen = vec![false; free.len()];
+    if !free[start] || occ.get(start) {
+        return Err(seen);
+    }
+    let mut prev = vec![usize::MAX; free.len()];
+    seen[start] = true;
+    let mut q = VecDeque::from([start]);
+    while let Some(u) = q.pop_front() {
+        if u == goal {
+            let mut path = vec![u];
+            let mut cur = u;
+            while cur != start {
+                cur = prev[cur];
+                path.push(cur);
+            }
+            path.reverse();
+            return Ok(path);
+        }
+        for nb in neighbors(u) {
+            if seen[nb] || !free[nb] || occ.get(nb) || !edge_ok(u, nb) {
+                continue;
+            }
+            seen[nb] = true;
+            prev[nb] = u;
+            q.push_back(nb);
+        }
+    }
+    Err(seen)
+}
+
+/// Route the connections in `order`, each taking a shortest path through the
+/// nodes its predecessors left free. Returns per-connection paths (indexed by
+/// connection, not by position in `order`) when every one succeeds — a
+/// node-disjoint joint routing by construction. `None` means only "this order
+/// did not work"; it is never evidence of infeasibility.
+fn sequential_bfs(
+    order: &[usize],
+    terms: &[(usize, usize)],
+    free: &[bool],
+    n_nodes: usize,
+    neighbors: &dyn Fn(usize) -> Vec<usize>,
+    edge_ok: &mut dyn FnMut(usize, usize) -> bool,
+) -> Option<Vec<Vec<usize>>> {
+    let mut occ = BitSet::new(n_nodes);
+    let mut paths = vec![Vec::new(); terms.len()];
+    for &i in order {
+        let (s, t) = terms[i];
+        if occ.get(t) {
+            return None;
+        }
+        let path = bfs_path(s, t, free, &occ, neighbors, edge_ok).ok()?;
+        for &node in &path {
+            occ.set(node);
+        }
+        paths[i] = path;
+    }
+    Some(paths)
+}
+
+/// Deterministic connection orders for the witness attempt: as given, longest
+/// terminal span first (the constrained nets pick their corridor before the
+/// short ones fill it), then shortest first.
+fn attempt_orders(terms: &[(usize, usize)], nx: usize, plane: usize) -> Vec<Vec<usize>> {
+    let span = |&(s, t): &(usize, usize)| {
+        let coords = |n: usize| ((n % plane) % nx, (n % plane) / nx, n / plane);
+        let (sx, sy, sl) = coords(s);
+        let (tx, ty, tl) = coords(t);
+        sx.abs_diff(tx) + sy.abs_diff(ty) + sl.abs_diff(tl)
+    };
+    let identity: Vec<usize> = (0..terms.len()).collect();
+    let mut longest = identity.clone();
+    longest.sort_by_key(|&i| (std::cmp::Reverse(span(&terms[i])), i));
+    let mut shortest = identity.clone();
+    shortest.sort_by_key(|&i| (span(&terms[i]), i));
+    let mut orders = vec![identity];
+    for order in [longest, shortest] {
+        if !orders.contains(&order) {
+            orders.push(order);
+        }
+    }
+    orders
+}
+
+/// Tally, per net, how many blockers stand between `geom` and legality on any
+/// of `layers`, for any of the candidate `nets` (net name, clearance).
+fn census_add(
+    census: &mut BTreeMap<String, usize>,
+    session: &RouteSession,
+    geom: &CopperGeom,
+    layers: &[PcbLayer],
+    nets: &[(&str, f64)],
+) {
+    for &layer in layers {
+        for &(net, clearance) in nets {
+            for blocker in session.probe(geom, layer, net, clearance).blockers {
+                *census.entry(blocker.net).or_default() += 1;
+            }
+        }
+    }
+}
+
+/// Nets whose copper blocks `geom`, as a census.
+fn blocking_nets(
+    session: &RouteSession,
+    geom: &CopperGeom,
+    layers: &[PcbLayer],
+    net: &str,
+    clearance: f64,
+) -> BTreeMap<String, usize> {
+    let mut census = BTreeMap::new();
+    census_add(&mut census, session, geom, layers, &[(net, clearance)]);
+    census
+}
+
+/// The heaviest few blockers, named: `"GND (61), /VDD_5V (4)"`.
+fn name_census(census: &BTreeMap<String, usize>) -> String {
+    if census.is_empty() {
+        return "copper the window's union-legality raster rejects for a sibling net".into();
+    }
+    let mut ranked: Vec<(&String, &usize)> = census.iter().collect();
+    ranked.sort_by(|a, b| b.1.cmp(a.1).then(a.0.cmp(b.0)));
+    ranked
+        .iter()
+        .take(3)
+        .map(|(net, n)| {
+            let named = if net.is_empty() { "<no net>" } else { net };
+            format!("{named} ({n})")
+        })
+        .collect::<Vec<_>>()
+        .join(", ")
+}
+
+/// Describe the ring of blocked nodes that encloses `reached` — the vertex cut
+/// the search ran into — by size, extent, and the copper that forms it.
+#[allow(clippy::too_many_arguments)]
+fn frontier_census(
+    session: &RouteSession,
+    grid: &WinGrid,
+    topo: &Topology,
+    net: &str,
+    clearance: f64,
+    free: &[bool],
+    reached: &[bool],
+    neighbors: &dyn Fn(usize) -> Vec<usize>,
+) -> String {
+    let mut cut: Vec<usize> = Vec::new();
+    let mut census: BTreeMap<String, usize> = BTreeMap::new();
+    let (mut lo, mut hi) = (
+        Vec2::new(f64::INFINITY, f64::INFINITY),
+        Vec2::new(f64::NEG_INFINITY, f64::NEG_INFINITY),
+    );
+    for (v, _) in reached.iter().enumerate().filter(|(_, r)| **r) {
+        for nb in neighbors(v) {
+            if reached[nb] {
+                continue;
+            }
+            cut.push(nb);
+            let p = grid.world(nb % topo.plane);
+            lo.x = lo.x.min(p.x);
+            lo.y = lo.y.min(p.y);
+            hi.x = hi.x.max(p.x);
+            hi.y = hi.y.max(p.y);
+            // The copper that forbids this step: the swept trace for an
+            // in-plane move, the via pad for a layer change.
+            let (la, ca) = (v / topo.plane, v % topo.plane);
+            let (lb, cb) = (nb / topo.plane, nb % topo.plane);
+            if la == lb {
+                let geom = CopperGeom::Segment {
+                    a: grid.world(ca),
+                    b: grid.world(cb),
+                    half_w: topo.half_w,
+                };
+                census_add(
+                    &mut census,
+                    session,
+                    &geom,
+                    &[topo.layers[la]],
+                    &[(net, clearance)],
+                );
+            } else {
+                let geom = CopperGeom::Disc {
+                    center: grid.world(ca),
+                    r: topo.via_r,
+                };
+                census_add(
+                    &mut census,
+                    session,
+                    &geom,
+                    &[topo.layers[la], topo.layers[lb]],
+                    &[(net, clearance)],
+                );
+            }
+        }
+    }
+    cut.sort_unstable();
+    cut.dedup();
+    if cut.is_empty() {
+        return format!(
+            "the {} free node{} it can reach have no blocked neighbour at all: the window \
+             itself is too small to leave the terminal's pocket",
+            free.iter().filter(|f| **f).count(),
+            if free.len() == 1 { "" } else { "s" }
+        );
+    }
+    format!(
+        "the enclosing cut is {} blocked node{} spanning x={:.2}..{:.2}, y={:.2}..{:.2}, held \
+         by {}",
+        cut.len(),
+        if cut.len() == 1 { "" } else { "s" },
+        lo.x - grid.pitch / 2.0,
+        hi.x + grid.pitch / 2.0,
+        lo.y - grid.pitch / 2.0,
+        hi.y + grid.pitch / 2.0,
+        name_census(&census),
+    )
+}
+
+/// Certificate for a lone connection whose terminals are severed on the
+/// canonical grid: what was exhausted, and which copper closed the door.
+#[allow(clippy::too_many_arguments)]
+fn severed_reason(
+    session: &RouteSession,
+    grid: &WinGrid,
+    topo: &Topology,
+    conn: &(String, Vec2, Vec2),
+    clearance: f64,
+    free: &[bool],
+    reached: &[bool],
+    neighbors: &dyn Fn(usize) -> Vec<usize>,
+    terms: (usize, usize),
+    from_side: bool,
+) -> String {
+    let (net, from, to) = conn;
+    let n_free = free.iter().filter(|f| **f).count();
+    let n_reached = reached.iter().filter(|r| **r).count();
+    let (searched, other, other_node) = if from_side {
+        (from, to, terms.1)
+    } else {
+        (to, from, terms.0)
+    };
+    format!(
+        "net {net} is severed inside the window: breadth-first search from its \
+         {} terminal at ({:.2}, {:.2}) exhausted every reachable node — {n_reached} of the \
+         {n_free} clearance-free (cell, layer) nodes on the {}-layer stack — without touching \
+         the other terminal at ({:.2}, {:.2}) (layer {:?}); {}. With k = 1 reachability is \
+         exact, so no path exists on the canonical grid at pitch {:.3} mm",
+        if from_side { "from" } else { "to" },
+        searched.x,
+        searched.y,
+        topo.layers.len(),
+        other.x,
+        other.y,
+        topo.layers[other_node / topo.plane],
+        frontier_census(session, grid, topo, net, clearance, free, reached, neighbors),
+        grid.pitch,
+    )
+}
+
 /// Max number of pairwise node-disjoint source→target paths through the free
 /// nodes (unit node capacities via node splitting), together with the cells
 /// of the min vertex cut when the flow is short. Pairing-agnostic: any source
@@ -732,17 +1432,26 @@ struct WinGrid {
 }
 
 impl WinGrid {
-    fn new(window: (Vec2, Vec2), width: f64, clearance: f64) -> Self {
+    fn new(
+        window: (Vec2, Vec2),
+        width: f64,
+        separation: f64,
+        drill_floor: f64,
+        max_axis_cells: usize,
+    ) -> Self {
         let (lo, hi) = window;
         let span_x = (hi.x - lo.x).max(1e-3);
         let span_y = (hi.y - lo.y).max(1e-3);
-        // 6% over the exact width+clearance floor: node-disjoint paths in
-        // adjacent columns sit at pitch - width — exactly the clearance at
+        // 6% over the exact width+separation floor: node-disjoint paths in
+        // adjacent columns sit at pitch - width — exactly the separation at
         // the floor, which board DRC then fails on floating-point margins.
-        let mut pitch = ((width + clearance) * 1.06).max(0.02);
+        let mut pitch = ((width + separation) * 1.06)
+            .max(0.02)
+            .max(drill_floor * 1.02);
+        let cap = max_axis_cells.max(2) as f64;
         let need = (span_x / pitch).max(span_y / pitch);
-        if need > MAX_AXIS_CELLS as f64 {
-            pitch = (span_x / MAX_AXIS_CELLS as f64).max(span_y / MAX_AXIS_CELLS as f64);
+        if need > cap {
+            pitch = (span_x / cap).max(span_y / cap);
         }
         let nx = (span_x / pitch).ceil() as usize + 1;
         let ny = (span_y / pitch).ceil() as usize + 1;
@@ -1030,11 +1739,101 @@ mod tests {
         assert_probe_legal(&session, &conns, &routed, 0.25);
     }
 
+    /// A lone connection is decided by reachability, which no budget can
+    /// interrupt: budget 1 must still answer, and answer definitively.
+    #[test]
+    fn one_connection_is_never_unknown() {
+        let pcb = board(vec![], &[PcbLayer::FCu, PcbLayer::BCu]);
+        let session = RouteSession::from_pcb(&pcb);
+        let conns = vec![(
+            "A".to_string(),
+            Vec2::new(12.0, 12.0),
+            Vec2::new(28.0, 28.0),
+        )];
+        let r = route_window_complete(&session, WINDOW, &[PcbLayer::FCu], &conns, 0.25, 1);
+        let CompleteOutcome::Routed(routed) = r else {
+            panic!("a reachable lone connection must route at any budget, got {r:?}");
+        };
+        assert_connected(&conns, &routed);
+        assert_probe_legal(&session, &conns, &routed, 0.25);
+    }
+
+    /// A lone connection walled off by foreign copper is *proved* infeasible —
+    /// never unknown — and the certificate names the cut it ran into.
+    #[test]
+    fn one_severed_connection_is_proved_with_a_named_cut() {
+        // A closed box of foreign copper around the source terminal.
+        let boxed = vec![
+            trace("GND", Vec2::new(11.0, 11.0), Vec2::new(13.0, 11.0)),
+            trace("GND", Vec2::new(13.0, 11.0), Vec2::new(13.0, 13.0)),
+            trace("GND", Vec2::new(13.0, 13.0), Vec2::new(11.0, 13.0)),
+            trace("GND", Vec2::new(11.0, 13.0), Vec2::new(11.0, 11.0)),
+        ];
+        let pcb = board(boxed, &[PcbLayer::FCu]);
+        let session = RouteSession::from_pcb(&pcb);
+        let conns = vec![(
+            "A".to_string(),
+            Vec2::new(12.0, 12.0),
+            Vec2::new(28.0, 28.0),
+        )];
+        let r = route_window_complete(&session, WINDOW, &[PcbLayer::FCu], &conns, 0.25, 2_000_000);
+        let CompleteOutcome::ProvedInfeasible { reason } = r else {
+            panic!("a boxed-in terminal must be proved infeasible, got {r:?}");
+        };
+        assert!(
+            reason.contains("GND"),
+            "certificate must name the copper forming the cut: {reason}"
+        );
+    }
+
+    /// Terminals pinned to a layer must attach there — a path that surfaces on
+    /// another layer would be electrically dangling.
     #[test]
-    fn tiny_budget_reports_unknown_never_infeasible() {
-        // Same (feasible) instance as the crossing test: with budget=1 the
-        // flow pre-pass passes, the DFS trips immediately, and the honest
-        // answer is BudgetExhausted — never a fake infeasibility proof.
+    fn pinned_terminals_attach_on_their_own_layer() {
+        let pcb = board(vec![], &[PcbLayer::FCu, PcbLayer::BCu]);
+        let session = RouteSession::from_pcb(&pcb);
+        let conns = vec![(
+            "A".to_string(),
+            Vec2::new(12.0, 12.0),
+            Vec2::new(28.0, 28.0),
+        )];
+        let pins = vec![TerminalLayers {
+            from: vec![PcbLayer::BCu],
+            to: vec![PcbLayer::BCu],
+        }];
+        let r = route_window_complete_pinned(
+            &session,
+            WINDOW,
+            &[PcbLayer::FCu, PcbLayer::BCu],
+            &conns,
+            &pins,
+            0.25,
+            None,
+            WindowBudget::new(2_000_000),
+        );
+        let CompleteOutcome::Routed(routed) = r else {
+            panic!("an empty board must route a pinned connection, got {r:?}");
+        };
+        assert_connected(&conns, &routed);
+        assert_eq!(
+            routed[0].first().map(|s| s.2),
+            Some(PcbLayer::BCu),
+            "the first segment must leave the pad on the pinned layer"
+        );
+        assert_eq!(
+            routed[0].last().map(|s| s.2),
+            Some(PcbLayer::BCu),
+            "the last segment must reach the pad on the pinned layer"
+        );
+    }
+
+    #[test]
+    fn tiny_budget_never_fakes_infeasibility() {
+        // Same (feasible) instance as the crossing test, with budget=1. The
+        // budget bounds the exhaustive DFS only: the sequential-BFS witness
+        // pass runs first and settles this instance, so the outcome here is a
+        // routing. What must never happen — at any budget — is a claim of
+        // infeasibility for an instance whose space was not exhausted.
         let pcb = board(vec![], &[PcbLayer::FCu, PcbLayer::BCu]);
         let session = RouteSession::from_pcb(&pcb);
         let conns = vec![
@@ -1063,8 +1862,13 @@ mod tests {
             1,
         );
         assert!(
-            matches!(r, CompleteOutcome::BudgetExhausted),
-            "budget=1 must yield BudgetExhausted, got {r:?}"
+            !matches!(r, CompleteOutcome::ProvedInfeasible { .. }),
+            "budget=1 must never yield an infeasibility proof, got {r:?}"
         );
+        let CompleteOutcome::Routed(routed) = r else {
+            panic!("the witness pass settles this feasible instance, got {r:?}");
+        };
+        assert_connected(&conns, &routed);
+        assert_probe_legal(&session, &conns, &routed, 0.25);
     }
 }
diff --git a/crates/vcad-ecad-pcb/src/session.rs b/crates/vcad-ecad-pcb/src/session.rs
index 099cc28c..af90d6ef 100644
--- a/crates/vcad-ecad-pcb/src/session.rs
+++ b/crates/vcad-ecad-pcb/src/session.rs
@@ -60,6 +60,40 @@ impl RTreeObject for SessionElement {
     }
 }
 
+/// A drilled hole (via barrel or through-hole pad) in the session's drill
+/// index. Holes are indexed apart from copper because the hole-to-hole rule is
+/// mechanical: it ignores nets *and* layers, so two vias whose layer spans never
+/// meet — a blind In1–In2 microvia and a buried In5–In6 one — are invisible to a
+/// layer-scoped copper probe yet still collide in the drill file.
+#[derive(Clone)]
+struct DrillElement {
+    center: Vec2,
+    radius: f64,
+}
+
+impl RTreeObject for DrillElement {
+    type Envelope = AABB<[f64; 2]>;
+
+    fn envelope(&self) -> Self::Envelope {
+        AABB::from_corners(
+            [self.center.x - self.radius, self.center.y - self.radius],
+            [self.center.x + self.radius, self.center.y + self.radius],
+        )
+    }
+}
+
+/// Result of a [`RouteSession::probe_drill`] hole-to-hole test.
+#[derive(Debug, Clone, PartialEq)]
+pub struct DrillProbe {
+    /// Whether the candidate hole satisfies the board's hole-to-hole rule.
+    pub legal: bool,
+    /// Closest edge-to-edge distance to an existing hole (mm); infinite when
+    /// the board has no other holes.
+    pub min_spacing: f64,
+    /// Centre of the nearest hole, when one was found.
+    pub nearest: Option<Vec2>,
+}
+
 /// A piece of existing copper found within the required clearance of a probed
 /// candidate.
 #[derive(Debug, Clone, PartialEq)]
@@ -161,11 +195,25 @@ pub struct RouteSession {
     /// probe enforces the pair GAP between the twins' leg-width copper, so no
     /// routing stage can emit an intra-pair pinch the DRC would flag.
     pair_rules: HashMap<String, (String, f64, f64)>,
+    /// Pad positions of the nets in `pair_rules` — the breakout regions where
+    /// the DRC relaxes the pair gap (see [`RouteSession::in_pair_breakout`]).
+    pair_pads: HashMap<String, Vec<Vec2>>,
+    /// Whether the intra-pair gap is scored the way the DRC scores it, including
+    /// against copper that carries no width of its own — see
+    /// [`RouteSession::set_strict_pair_coupling`].
+    strict_pair_coupling: bool,
     default_clearance: f64,
     /// Largest clearance any net requires — the broadphase must reach this far
     /// so a wide net's clearance is never missed when it exceeds the candidate's.
     max_clearance: f64,
     net_width: HashMap<String, f64>,
+    /// Every drilled hole on the board, for the layer- and net-agnostic
+    /// hole-to-hole rule (see [`DrillElement`]).
+    drills: RTree<DrillElement>,
+    /// Largest indexed drill radius — the broadphase reach for a drill probe.
+    max_drill_radius: f64,
+    /// The board's minimum hole-to-hole edge spacing (mm).
+    hole_to_hole: f64,
     /// Per-span bboxes (parallel to `live`), so a remove can stamp the dirty
     /// grid without consulting the tree.
     bounds: Vec<[f64; 4]>,
@@ -272,6 +320,24 @@ impl RouteSession {
             .values()
             .copied()
             .fold(default_clearance, f64::max);
+        let drills = drill_elements(pcb);
+        let max_drill_radius = drills.iter().map(|d| d.radius).fold(0.0_f64, f64::max);
+        let pair_nets: std::collections::HashSet<String> = crate::drc::diff_pairs(pcb)
+            .into_iter()
+            .flat_map(|dp| [dp.net_p, dp.net_n])
+            .collect();
+        let mut pair_pads: HashMap<String, Vec<Vec2>> = HashMap::new();
+        for fp in &pcb.footprints {
+            for pad in &fp.pads {
+                let Some(net) = pad.net.as_ref().filter(|n| pair_nets.contains(*n)) else {
+                    continue;
+                };
+                pair_pads
+                    .entry(net.clone())
+                    .or_default()
+                    .push(crate::geometry::pad_world_position(fp, pad));
+            }
+        }
         Self {
             tree: RTree::bulk_load(session_elems),
             live,
@@ -286,9 +352,14 @@ impl RouteSession {
                 }
                 m
             },
+            pair_pads,
+            strict_pair_coupling: false,
             default_clearance,
             max_clearance,
             net_width: build_net_trace_width_map(pcb),
+            drills: RTree::bulk_load(drills),
+            max_drill_radius,
+            hole_to_hole: pcb.rules.hole_to_hole,
             bounds,
             dirty,
             change_epoch: 0,
@@ -316,6 +387,113 @@ impl RouteSession {
             .unwrap_or(self.default_clearance)
     }
 
+    /// Test a candidate drilled hole against every hole already on the board.
+    ///
+    /// Nets and layers are deliberately ignored: hole-to-hole is a mechanical
+    /// rule about the drill file, and it is the one legality question a copper
+    /// probe structurally cannot answer — two vias on disjoint layer spans share
+    /// no layer, so no layer-scoped probe ever compares them, and they land as
+    /// drill collisions the DRC only finds after the fact.
+    pub fn probe_drill(&self, center: Vec2, diameter: f64) -> DrillProbe {
+        let r = diameter / 2.0;
+        let reach = r + self.max_drill_radius + self.hole_to_hole;
+        let mut min_spacing = f64::INFINITY;
+        let mut nearest = None;
+        for hole in self
+            .drills
+            .locate_in_envelope_intersecting(&AABB::from_corners(
+                [center.x - reach, center.y - reach],
+                [center.x + reach, center.y + reach],
+            ))
+        {
+            let d = ((hole.center.x - center.x).powi(2) + (hole.center.y - center.y).powi(2))
+                .sqrt()
+                - hole.radius
+                - r;
+            if d < min_spacing {
+                min_spacing = d;
+                nearest = Some(hole.center);
+            }
+        }
+        DrillProbe {
+            legal: min_spacing >= self.hole_to_hole - 1e-6,
+            min_spacing,
+            nearest,
+        }
+    }
+
+    /// Score the intra-pair gap exactly as the DRC does — including against a
+    /// twin's pads and via annuli, which carry no width of their own and which
+    /// `drc::pair_aware_clearance_w` therefore treats as coupled leg copper.
+    ///
+    /// Off by default, because it is *stricter* than the geometry the pair
+    /// router currently realizes: its dog-bone offsets and jogs are sized to the
+    /// base clearance, so turning this on globally would stop pairs from
+    /// changing layers rather than making them legal (see the twin-clearance
+    /// tests in `router::pair`). A caller that must not emit copper the board
+    /// DRC will flag — the verdict driver, which commits fail-closed — turns it
+    /// on and pays for it in routability instead.
+    pub fn set_strict_pair_coupling(&mut self, strict: bool) {
+        self.strict_pair_coupling = strict;
+    }
+
+    /// Whether a candidate/blocker pair sits in a twin's **pad breakout**, where
+    /// the DRC relaxes the intra-pair gap to the base clearance.
+    ///
+    /// Mirrors `drc::check_clearance`: the gap binds the coupled run, not the
+    /// escape region (1.5 mm) around either twin's own pads, where the legs must
+    /// converge to reach their land patterns. The DRC judges a pair from the
+    /// *trace* side, so copper with no endpoints of its own — a via annulus or a
+    /// pad — imposes nothing from its side of the comparison.
+    fn in_pair_breakout(
+        &self,
+        cand: &CopperGeom,
+        blocker: &CopperGeom,
+        net: &str,
+        twin: &str,
+    ) -> bool {
+        const BREAKOUT_MM: f64 = 1.5;
+        let near_pad =
+            |p: Vec2| {
+                [net, twin].iter().any(|n| {
+                    self.pair_pads.get(*n).into_iter().flatten().any(|q| {
+                        (q.x - p.x).powi(2) + (q.y - p.y).powi(2) <= BREAKOUT_MM * BREAKOUT_MM
+                    })
+                })
+            };
+        let side = |g: &CopperGeom| match g {
+            CopperGeom::Segment { a, b, .. } => near_pad(*a) || near_pad(*b),
+            _ => true,
+        };
+        side(cand) && side(blocker)
+    }
+
+    /// The board's minimum hole-to-hole edge spacing (mm).
+    pub fn hole_to_hole(&self) -> f64 {
+        self.hole_to_hole
+    }
+
+    /// Index a drilled hole so later [`RouteSession::probe_drill`] calls see it.
+    /// Call this for every via a router commits — the copper commit alone leaves
+    /// the barrel invisible to the hole-to-hole rule.
+    pub fn commit_drill(&mut self, center: Vec2, diameter: f64) {
+        let radius = diameter / 2.0;
+        self.max_drill_radius = self.max_drill_radius.max(radius);
+        self.drills.insert(DrillElement { center, radius });
+    }
+
+    /// The declared intra-pair gap between `net` and `other` when the two are
+    /// twins of a differential pair, else `None`. This is the separation the
+    /// probe demands between their leg-width copper, so a router that must keep
+    /// two candidate paths mutually legal has to space them by at least this
+    /// much — not merely by the base clearance.
+    pub fn pair_gap_between(&self, net: &str, other: &str) -> Option<f64> {
+        self.pair_rules
+            .get(net)
+            .filter(|(twin, _, _)| twin == other)
+            .map(|&(_, gap, _)| gap)
+    }
+
     /// The trace width for `net` from its net class, or `fallback` if the net
     /// has no class width (so power/ground classes route wider than signals).
     pub fn width_for(&self, net: &str, fallback: f64) -> f64 {
@@ -532,11 +710,18 @@ impl RouteSession {
             // base clearance — the uncoupled entry region.
             if let Some((twin, gap, leg_w)) = self.pair_rules.get(net) {
                 if &e.net == twin {
-                    let fat = |g: &CopperGeom| match g {
+                    // Which copper counts as a coupled leg. Segments count at
+                    // (nearly) the leg width — a thinner neck is the uncoupled
+                    // entry by definition. Copper with no width of its own (a
+                    // pad, a via annulus) counts only in strict mode, which is
+                    // how `drc::pair_aware_clearance_w` scores it.
+                    let strict = self.strict_pair_coupling;
+                    let leg = |g: &CopperGeom| match g {
                         CopperGeom::Segment { half_w, .. } => 2.0 * half_w >= leg_w - 0.01,
-                        _ => false,
+                        _ => strict,
                     };
-                    if fat(geom) && fat(&e.geom) {
+                    if leg(geom) && leg(&e.geom) && !self.in_pair_breakout(geom, &e.geom, net, twin)
+                    {
                         required = required.max(gap - 0.005);
                     }
                 }
@@ -559,6 +744,31 @@ impl RouteSession {
     }
 }
 
+/// Every drilled hole on `pcb`: via barrels and through-hole pads. Mirrors the
+/// DRC's own hole census (`check_hole_to_hole`), so the router's answer and the
+/// board's verdict cannot disagree.
+fn drill_elements(pcb: &Pcb) -> Vec<DrillElement> {
+    let mut out: Vec<DrillElement> = pcb
+        .vias
+        .iter()
+        .map(|via| DrillElement {
+            center: via.position,
+            radius: via.drill / 2.0,
+        })
+        .collect();
+    for fp in &pcb.footprints {
+        for pad in &fp.pads {
+            if let Some(drill) = &pad.drill {
+                out.push(DrillElement {
+                    center: crate::geometry::pad_world_position(fp, pad),
+                    radius: drill.diameter / 2.0,
+                });
+            }
+        }
+    }
+    out
+}
+
 /// Axis-aligned bounding box (copper extent) of a [`CopperGeom`].
 fn geom_aabb(g: &CopperGeom) -> ([f64; 2], [f64; 2]) {
     match g {
@@ -824,6 +1034,56 @@ mod tests {
         assert!(r.legal, "net-tied copper must be exempt");
     }
 
+    /// Drills are compared across layer spans and nets, because that is what
+    /// the fab file says: two vias whose copper never shares a layer still
+    /// collide in the drill. This is the one legality question the copper probe
+    /// structurally cannot answer.
+    #[test]
+    fn drill_probe_sees_holes_no_copper_probe_could() {
+        let mut pcb = empty_pcb();
+        pcb.vias.push(vcad_ir::ecad::Via {
+            position: Vec2::new(50.0, 50.0),
+            diameter: 0.8,
+            drill: 0.4,
+            start_layer: PcbLayer::In1Cu,
+            end_layer: PcbLayer::In2Cu,
+            net: "GND".into(),
+            source: None,
+        });
+        let mut session = RouteSession::from_pcb(&pcb);
+        // hole_to_hole is 0.5 here: edge distance must be at least that.
+        let touching = session.probe_drill(Vec2::new(50.4, 50.0), 0.4);
+        assert!(
+            !touching.legal && touching.min_spacing < 0.5,
+            "a hole 0.4mm away (edge 0.0mm) must be illegal, got {touching:?}"
+        );
+        assert_eq!(touching.nearest, Some(Vec2::new(50.0, 50.0)));
+        let clear = session.probe_drill(Vec2::new(51.5, 50.0), 0.4);
+        assert!(
+            clear.legal,
+            "a hole 1.5mm away must be legal, got {clear:?}"
+        );
+        // A copper probe on a layer the existing via does not span sees nothing
+        // there at all — hence the separate index.
+        assert!(
+            session
+                .probe(
+                    &CopperGeom::Disc {
+                        center: Vec2::new(50.4, 50.0),
+                        r: 0.4,
+                    },
+                    PcbLayer::In5Cu,
+                    "SIG",
+                    0.2,
+                )
+                .legal,
+            "the copper probe cannot see a hole on an unshared layer"
+        );
+        // Newly committed drills join the index.
+        session.commit_drill(Vec2::new(60.0, 60.0), 0.4);
+        assert!(!session.probe_drill(Vec2::new(60.3, 60.0), 0.4).legal);
+    }
+
     #[test]
     fn ids_stay_stable_across_compaction() {
         let mut session = RouteSession::from_pcb(&empty_pcb());