diff --git a/tests/idris2/AspectSecurityTest.idr b/tests/idris2/AspectSecurityTest.idr
new file mode 100644
index 0000000..c6a745c
--- /dev/null
+++ b/tests/idris2/AspectSecurityTest.idr
@@ -0,0 +1,208 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Port of tests/aspect/security_aspect_test.ts to Idris2, estate-rollout 9/11.
+-- 13 of 13 aspect tests ported.
+--
+-- The TS suite uses /[a-zA-Z0-9]{N,}/-style regexes to detect long alnum
+-- runs that aren't EXAMPLE/CHANGEME placeholders. We re-derive longest-run
+-- length as a pure helper (see ContractNetworkContractsTest.idr for the
+-- twin) and gate on the absence-of-placeholder for the file as a whole.
+
+module AspectSecurityTest
+
+import Test.Spec
+import Data.String
+import Data.List
+import System.File
+
+%default covering
+
+-- File helpers ---------------------------------------------------------------
+
+readFileToString : String -> IO String
+readFileToString path = do
+  Right contents <- readFile path
+    | Left _ => pure ""
+  pure contents
+
+-- Pure helpers ---------------------------------------------------------------
+
+isAlnum : Char -> Bool
+isAlnum c =
+     (c >= '0' && c <= '9')
+  || (c >= 'a' && c <= 'z')
+  || (c >= 'A' && c <= 'Z')
+
+longestAlnumRun : List Char -> Nat
+longestAlnumRun = go 0 0
+  where
+    go : Nat -> Nat -> List Char -> Nat
+    go best _   []        = best
+    go best cur (c :: cs) =
+      if isAlnum c
+        then let cur' = S cur
+                 best' = if cur' > best then cur' else best
+             in go best' cur' cs
+        else go best 0 cs
+
+-- `safeFromLongAlnum content`: True iff the file either has no 20+
+-- alphanumeric run, OR contains an EXAMPLE/CHANGEME placeholder (so the
+-- long run is plausibly a placeholder, not a real credential).
+safeFromLongAlnum : Nat -> String -> Bool
+safeFromLongAlnum threshold content =
+  let run = longestAlnumRun (unpack content)
+      hasPlaceholder = isInfixOf "EXAMPLE" content || isInfixOf "CHANGEME" content
+  in run < threshold || hasPlaceholder
+
+public export
+allSuites : List TestCase
+allSuites =
+  [ test "Aspect: No hardcoded API keys in network config" $ do
+      content <- readFileToString "configs/network.ncl"
+      allPass
+        [ assertTrue "no 32+ alnum run without CHANGEME"
+            (safeFromLongAlnum 32 content)
+        , assertTrue "no sk_live_ Stripe pattern"
+            (not (isInfixOf "sk_live_" content))
+        , assertTrue "no zt_ literal token pattern (allow zt+ interface)"
+            (not (isInfixOf "zt_real" content))
+        ]
+
+  , test "Aspect: No hardcoded tokens in daemonset" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      -- If ZEROTIER_* env-var names appear, secretKeyRef or configMapKeyRef
+      -- must also appear (i.e. they come from references, not literals).
+      let hasZTEnv = isInfixOf "ZEROTIER_" content
+      let hasSecretRef = isInfixOf "secretKeyRef" content
+                     || isInfixOf "configMapKeyRef" content
+      assertTrue "ZEROTIER_* env vars use secretKeyRef/configMapKeyRef"
+        (not hasZTEnv || hasSecretRef)
+
+  , test "Aspect: No HTTP endpoints (HTTPS only)" $ do
+      a <- readFileToString "configs/network.ncl"
+      b <- readFileToString "configs/firewall.ncl"
+      c <- readFileToString "configs/routes.ncl"
+      d <- readFileToString "manifests/daemonset.yaml"
+      e <- readFileToString "manifests/networkpolicy.yaml"
+      allPass
+        [ assertTrue "no http:// in network.ncl"        (not (isInfixOf "http://" a))
+        , assertTrue "no http:// in firewall.ncl"       (not (isInfixOf "http://" b))
+        , assertTrue "no http:// in routes.ncl"         (not (isInfixOf "http://" c))
+        , assertTrue "no http:// in daemonset.yaml"     (not (isInfixOf "http://" d))
+        , assertTrue "no http:// in networkpolicy.yaml" (not (isInfixOf "http://" e))
+        ]
+
+  , test "Aspect: No world-readable permission patterns (chmod 777)" $ do
+      a <- readFileToString "scripts/authorize-nodes.sh"
+      b <- readFileToString "scripts/configure-routes.sh"
+      c <- readFileToString "scripts/health-check.sh"
+      d <- readFileToString "scripts/join-network.sh"
+      e <- readFileToString "setup.sh"
+      let bad : String -> Bool
+          bad = \s => isInfixOf "chmod 777" s || isInfixOf "chmod a+rwx" s
+      allPass
+        [ assertTrue "authorize-nodes.sh"  (not (bad a))
+        , assertTrue "configure-routes.sh" (not (bad b))
+        , assertTrue "health-check.sh"     (not (bad c))
+        , assertTrue "join-network.sh"     (not (bad d))
+        , assertTrue "setup.sh"            (not (bad e))
+        ]
+
+  , test "Aspect: ZeroTier auth tokens are placeholders only" $ do
+      content <- readFileToString "manifests/secret.yaml"
+      let hasPlaceholder = isInfixOf "EXAMPLE_API_TOKEN" content
+                        && isInfixOf "EXAMPLE_NETWORK_ID" content
+      allPass
+        [ assertTrue "EXAMPLE_API_TOKEN + EXAMPLE_NETWORK_ID placeholders" hasPlaceholder
+        , assertTrue "no 20+ alnum run without EXAMPLE/CHANGEME"
+            (safeFromLongAlnum 20 content)
+        ]
+
+  , test "Aspect: NetworkPolicy has both ingress and egress rules" $ do
+      content <- readFileToString "manifests/networkpolicy.yaml"
+      allPass
+        [ assertTrue "ingress: present"  (isInfixOf "ingress:" content)
+        , assertTrue "egress: present"   (isInfixOf "egress:" content)
+        , assertTrue "ingress not empty" (not (isInfixOf "ingress: []" content))
+        , assertTrue "egress not empty"  (not (isInfixOf "egress: []" content))
+        ]
+
+  , test "Aspect: No plaintext passwords in manifests" $ do
+      -- A literal `password:` or `passwd:` key would be flagged. We mirror by
+      -- asserting none of these keys appears in the manifests at all.
+      a <- readFileToString "manifests/configmap.yaml"
+      b <- readFileToString "manifests/daemonset.yaml"
+      c <- readFileToString "manifests/namespace.yaml"
+      d <- readFileToString "manifests/networkpolicy.yaml"
+      e <- readFileToString "manifests/secret.yaml"
+      f <- readFileToString "manifests/servicemonitor.yaml"
+      let noPwd : String -> Bool
+          noPwd = \s => not (isInfixOf "password:" s) && not (isInfixOf "passwd:" s)
+      allPass
+        [ assertTrue "configmap.yaml"      (noPwd a)
+        , assertTrue "daemonset.yaml"      (noPwd b)
+        , assertTrue "namespace.yaml"      (noPwd c)
+        , assertTrue "networkpolicy.yaml"  (noPwd d)
+        , assertTrue "secret.yaml"         (noPwd e)
+        , assertTrue "servicemonitor.yaml" (noPwd f)
+        ]
+
+  , test "Aspect: No exposure of internal credentials via logs" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      allPass
+        [ assertTrue "no echo $ZEROTIER_NETWORK_ID"
+            (not (isInfixOf "echo \"$ZEROTIER_NETWORK_ID" content))
+        , assertTrue "no echo $ZEROTIER_API_TOKEN"
+            (not (isInfixOf "echo \"$ZEROTIER_API_TOKEN" content))
+        ]
+
+  , test "Aspect: Firewall denies by default (principle of least privilege)" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      let outputDecl = isInfixOf "output_policy = \"ACCEPT\"" content
+                    || isInfixOf "output_policy = \"DROP\"" content
+      allPass
+        [ assertTrue "input_policy = DROP"   (isInfixOf "input_policy = \"DROP\"" content)
+        , assertTrue "forward_policy = DROP" (isInfixOf "forward_policy = \"DROP\"" content)
+        , assertTrue "output_policy decided" outputDecl
+        ]
+
+  , test "Aspect: DaemonSet security context restricts container capabilities" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      assertTrue "securityContext: present" (isInfixOf "securityContext:" content)
+
+  , test "Aspect: No hardcoded secrets in scripts" $ do
+      a <- readFileToString "scripts/authorize-nodes.sh"
+      b <- readFileToString "scripts/configure-routes.sh"
+      c <- readFileToString "scripts/health-check.sh"
+      d <- readFileToString "scripts/join-network.sh"
+      e <- readFileToString "setup.sh"
+      allPass
+        [ assertTrue "authorize-nodes.sh no 32+ alnum without placeholder/var"
+            (safeFromLongAlnum 32 a || isInfixOf "${" a)
+        , assertTrue "configure-routes.sh no 32+ alnum without placeholder/var"
+            (safeFromLongAlnum 32 b || isInfixOf "${" b)
+        , assertTrue "health-check.sh no 32+ alnum without placeholder/var"
+            (safeFromLongAlnum 32 c || isInfixOf "${" c)
+        , assertTrue "join-network.sh no 32+ alnum without placeholder/var"
+            (safeFromLongAlnum 32 d || isInfixOf "${" d)
+        , assertTrue "setup.sh no 32+ alnum without placeholder/var"
+            (safeFromLongAlnum 32 e || isInfixOf "${" e)
+        ]
+
+  , test "Aspect: Network config disables dangerous capabilities" $ do
+      content <- readFileToString "configs/network.ncl"
+      allPass
+        [ assertTrue "allow_global_ips = false"   (isInfixOf "allow_global_ips = false" content)
+        , assertTrue "allow_default_route = false" (isInfixOf "allow_default_route = false" content)
+        ]
+
+  , test "Aspect: Kubernetes RBAC references are appropriate" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      assertTrue "no cluster-admin role" (not (isInfixOf "cluster-admin" content))
+
+  , test "Aspect: Secret is type Opaque not other types" $ do
+      content <- readFileToString "manifests/secret.yaml"
+      assertTrue "type Opaque"
+        (isInfixOf "type: Opaque" content || isInfixOf "type: \"Opaque\"" content)
+  ]
diff --git a/tests/idris2/ContractNetworkContractsTest.idr b/tests/idris2/ContractNetworkContractsTest.idr
new file mode 100644
index 0000000..c7c2e7f
--- /dev/null
+++ b/tests/idris2/ContractNetworkContractsTest.idr
@@ -0,0 +1,234 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Port of tests/contract/network_contracts_test.ts to Idris2, estate-rollout 9/11.
+-- 18 of 18 contract INVARIANTS ported.
+--
+-- INVARIANT 3 (private-IP-only) in the TS suite walks the file with a regex
+-- to extract every IPv4 literal and check it falls in 10/172.16-31/192.168.
+-- Idris2's base stdlib has no regex; we re-implement IPv4 extraction +
+-- private-range membership as pure Idris2 (isPrivateIPv4) and walk the file
+-- contents character-by-character to find dotted-quads. This preserves the
+-- test's intent: every IPv4 literal in the config must be in a private range.
+--
+-- INVARIANT 4 ("no real credentials") similarly uses /[a-zA-Z0-9]{20,}/ to
+-- spot long alphanumeric runs that aren't EXAMPLE placeholders. We re-derive
+-- the longest alphanumeric run length as a pure helper and gate on
+-- absence-of-EXAMPLE for the file as a whole, matching the TS behaviour.
+
+module ContractNetworkContractsTest
+
+import Test.Spec
+import Data.String
+import Data.List
+import System.File
+
+%default covering
+
+-- File helpers ---------------------------------------------------------------
+
+readFileToString : String -> IO String
+readFileToString path = do
+  Right contents <- readFile path
+    | Left _ => pure ""
+  pure contents
+
+-- Pure helpers: digit/alnum classification -----------------------------------
+
+isDigitC : Char -> Bool
+isDigitC c = c >= '0' && c <= '9'
+
+isAlnum : Char -> Bool
+isAlnum c =
+     (c >= '0' && c <= '9')
+  || (c >= 'a' && c <= 'z')
+  || (c >= 'A' && c <= 'Z')
+
+-- Pure helpers: dotted-quad extraction and private-range membership ----------
+
+-- Parse a single decimal octet from the leading chars of `xs`.
+-- Returns (value, remainder) on success, Nothing on failure.
+parseOctet : List Char -> Maybe (Nat, List Char)
+parseOctet xs =
+  let digits = takeWhile isDigitC xs
+      rest   = dropWhile isDigitC xs
+  in if length digits == 0 || length digits > 3
+       then Nothing
+       else case parsePositive (pack digits) of
+              Just n  => if n <= 255 then Just (n, rest) else Nothing
+              Nothing => Nothing
+
+-- Try to parse "d.d.d.d" starting at the head of `xs`. Returns the 4 octets
+-- and the post-quad remainder on success, Nothing otherwise.
+parseDottedQuad : List Char -> Maybe (Nat, Nat, Nat, Nat, List Char)
+parseDottedQuad xs = do
+  (a, r1) <- parseOctet xs
+  case r1 of
+    ('.' :: r1') => do
+      (b, r2) <- parseOctet r1'
+      case r2 of
+        ('.' :: r2') => do
+          (c, r3) <- parseOctet r2'
+          case r3 of
+            ('.' :: r3') => do
+              (d, r4) <- parseOctet r3'
+              Just (a, b, c, d, r4)
+            _ => Nothing
+        _ => Nothing
+    _ => Nothing
+
+-- Walk a character list and collect every IPv4 dotted-quad we encounter,
+-- regardless of surrounding context. Mirrors the TS regex /\d+\.\d+\.\d+\.\d+/g.
+extractIPv4s : List Char -> List (Nat, Nat, Nat, Nat)
+extractIPv4s [] = []
+extractIPv4s xs@(_ :: rest) =
+  case parseDottedQuad xs of
+    Just (a, b, c, d, r) => (a, b, c, d) :: extractIPv4s r
+    Nothing              => extractIPv4s rest
+
+-- Private-range membership: 10/8, 172.16/12, 192.168/16.
+isPrivateIPv4 : (Nat, Nat, Nat, Nat) -> Bool
+isPrivateIPv4 (a, b, _, _) =
+     a == 10
+  || (a == 172 && b >= 16 && b <= 31)
+  || (a == 192 && b == 168)
+
+allPrivateIPv4s : String -> Bool
+allPrivateIPv4s content =
+  let ips = extractIPv4s (unpack content) in
+  all isPrivateIPv4 ips
+
+-- Longest run of alnum characters (mirrors /[a-zA-Z0-9]{N,}/ length check).
+longestAlnumRun : List Char -> Nat
+longestAlnumRun = go 0 0
+  where
+    go : Nat -> Nat -> List Char -> Nat
+    go best _   []        = best
+    go best cur (c :: cs) =
+      if isAlnum c
+        then let cur' = S cur
+                 best' = if cur' > best then cur' else best
+             in go best' cur' cs
+        else go best 0 cs
+
+public export
+allSuites : List TestCase
+allSuites =
+  [ test "Contract: INVARIANT - Firewall must have default deny rule for input" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      assertTrue "input_policy = DROP" (isInfixOf "input_policy = \"DROP\"" content)
+
+  , test "Contract: INVARIANT - Firewall must have default deny rule for forward" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      assertTrue "forward_policy = DROP" (isInfixOf "forward_policy = \"DROP\"" content)
+
+  , test "Contract: INVARIANT - ZeroTier network config uses private IP ranges only" $ do
+      content <- readFileToString "configs/network.ncl"
+      assertTrue "all dotted-quad IPv4 literals are RFC1918 private"
+        (allPrivateIPv4s content)
+
+  , test "Contract: INVARIANT - Kubernetes Secret must not have real credentials" $ do
+      content <- readFileToString "manifests/secret.yaml"
+      let hasPlaceholder = isInfixOf "EXAMPLE" content || isInfixOf "CHANGEME" content
+      -- Real ZT tokens are typically alphanumeric runs of 20+ chars. We
+      -- conservatively require any 20+ alphanumeric run to live in the
+      -- shadow of an EXAMPLE/CHANGEME placeholder.
+      let longestRun = longestAlnumRun (unpack content)
+      let noUnshieldedRun = (longestRun < 20) || hasPlaceholder
+      allPass
+        [ assertTrue "has EXAMPLE or CHANGEME placeholder" hasPlaceholder
+        , assertTrue "no 20+ alphanumeric run outside placeholder context" noUnshieldedRun
+        ]
+
+  , test "Contract: INVARIANT - NetworkPolicy must restrict ingress rules" $ do
+      content <- readFileToString "manifests/networkpolicy.yaml"
+      allPass
+        [ assertTrue "ingress: present"   (isInfixOf "ingress:" content)
+        , assertTrue "ingress not empty"  (not (isInfixOf "ingress: []" content))
+        ]
+
+  , test "Contract: INVARIANT - NetworkPolicy must restrict egress rules" $ do
+      content <- readFileToString "manifests/networkpolicy.yaml"
+      allPass
+        [ assertTrue "egress: present"   (isInfixOf "egress:" content)
+        , assertTrue "egress not empty"  (not (isInfixOf "egress: []" content))
+        ]
+
+  , test "Contract: INVARIANT - DaemonSet namespace matches namespace.yaml" $ do
+      -- The TS check both extracts the daemonset's `namespace:` value and
+      -- the namespace.yaml `metadata.name` value and asserts equality. We
+      -- mirror by asserting both files reference the same well-known name.
+      daemonset <- readFileToString "manifests/daemonset.yaml"
+      ns        <- readFileToString "manifests/namespace.yaml"
+      allPass
+        [ assertTrue "daemonset uses zerotier-system" (isInfixOf "namespace: zerotier-system" daemonset)
+        , assertTrue "namespace declares zerotier-system" (isInfixOf "zerotier-system" ns)
+        ]
+
+  , test "Contract: INVARIANT - All ABI files must have module declarations" $ do
+      a <- readFileToString "src/abi/Layout.idr"
+      b <- readFileToString "src/abi/Types.idr"
+      c <- readFileToString "src/abi/Foreign.idr"
+      allPass
+        [ assertTrue "Layout.idr has module"  (isInfixOf "module" a)
+        , assertTrue "Types.idr has module"   (isInfixOf "module" b)
+        , assertTrue "Foreign.idr has module" (isInfixOf "module" c)
+        ]
+
+  , test "Contract: INVARIANT - Network config must define both IPv4 and IPv6" $ do
+      content <- readFileToString "configs/network.ncl"
+      allPass
+        [ assertTrue "ipv4_assignment_pool" (isInfixOf "ipv4_assignment_pool" content)
+        , assertTrue "ipv6_assignment_pool" (isInfixOf "ipv6_assignment_pool" content)
+        ]
+
+  , test "Contract: INVARIANT - Routes reference at least one CIDR" $ do
+      content <- readFileToString "configs/routes.ncl"
+      let hasCidrTarget      = isInfixOf "target = \""      content
+      let hasCidrDestination = isInfixOf "destination = \"" content
+      let hasSlash           = isInfixOf "/24" content || isInfixOf "/48" content
+      allPass
+        [ assertTrue "has target/destination key" (hasCidrTarget || hasCidrDestination)
+        , assertTrue "has slash prefix"           hasSlash
+        ]
+
+  , test "Contract: INVARIANT - Firewall must have zerotier zone definition" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      assertTrue "zerotier zone present" (isInfixOf "zerotier" content)
+
+  , test "Contract: INVARIANT - DaemonSet must request privileged capabilities" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      assertTrue "NET_ADMIN capability" (isInfixOf "NET_ADMIN" content)
+
+  , test "Contract: INVARIANT - DaemonSet must use hostNetwork=true" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      assertTrue "hostNetwork: true" (isInfixOf "hostNetwork: true" content)
+
+  , test "Contract: INVARIANT - ConfigMap must be named zerotier-config" $ do
+      content <- readFileToString "manifests/configmap.yaml"
+      assertTrue "zerotier-config" (isInfixOf "zerotier-config" content)
+
+  , test "Contract: INVARIANT - Secret must be named zerotier-credentials" $ do
+      content <- readFileToString "manifests/secret.yaml"
+      assertTrue "zerotier-credentials" (isInfixOf "zerotier-credentials" content)
+
+  , test "Contract: INVARIANT - Network config must not allow default route via ZT" $ do
+      content <- readFileToString "configs/network.ncl"
+      assertTrue "allow_default_route = false"
+        (isInfixOf "allow_default_route = false" content)
+
+  , test "Contract: INVARIANT - Firewall control plane rule must use port 9993" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      assertTrue "9993" (isInfixOf "9993" content)
+
+  , test "Contract: INVARIANT - All config files must have SPDX headers" $ do
+      let spdx = "SPDX-License-Identifier"
+      a <- readFileToString "configs/network.ncl"
+      b <- readFileToString "configs/firewall.ncl"
+      c <- readFileToString "configs/routes.ncl"
+      allPass
+        [ assertTrue "network.ncl SPDX"  (isInfixOf spdx a)
+        , assertTrue "firewall.ncl SPDX" (isInfixOf spdx b)
+        , assertTrue "routes.ncl SPDX"   (isInfixOf spdx c)
+        ]
+  ]
diff --git a/tests/idris2/E2ENetworkTest.idr b/tests/idris2/E2ENetworkTest.idr
new file mode 100644
index 0000000..3f2824d
--- /dev/null
+++ b/tests/idris2/E2ENetworkTest.idr
@@ -0,0 +1,132 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Port of tests/e2e/network_e2e_test.ts to Idris2, estate-rollout 9/11.
+-- 12 of 12 end-to-end pipeline tests ported. The "e2e" suite in the TS
+-- original is itself purely file-read + substring-matching across multiple
+-- artefacts (no live cluster traffic), so it ports cleanly as bucket-1.
+
+module E2ENetworkTest
+
+import Test.Spec
+import Data.String
+import System.File
+
+%default covering
+
+readFileToString : String -> IO String
+readFileToString path = do
+  Right contents <- readFile path
+    | Left _ => pure ""
+  pure contents
+
+public export
+allSuites : List TestCase
+allSuites =
+  [ test "E2E: full config pipeline - read all Nickel configs" $ do
+      a <- readFileToString "configs/network.ncl"
+      b <- readFileToString "configs/firewall.ncl"
+      c <- readFileToString "configs/routes.ncl"
+      allPass
+        [ assertTrue "network.ncl non-empty"  (length a > 0)
+        , assertTrue "firewall.ncl non-empty" (length b > 0)
+        , assertTrue "routes.ncl non-empty"   (length c > 0)
+        ]
+
+  , test "E2E: K8s daemonset references correct namespace" $ do
+      daemonset <- readFileToString "manifests/daemonset.yaml"
+      ns        <- readFileToString "manifests/namespace.yaml"
+      allPass
+        [ assertTrue "daemonset namespace: zerotier-system"
+            (isInfixOf "namespace: zerotier-system" daemonset)
+        , assertTrue "namespace.yaml declares zerotier-system"
+            (isInfixOf "zerotier-system" ns)
+        ]
+
+  , test "E2E: NetworkPolicy references zerotier app labels" $ do
+      policy    <- readFileToString "manifests/networkpolicy.yaml"
+      daemonset <- readFileToString "manifests/daemonset.yaml"
+      let lbl = "app.kubernetes.io/name: zerotier"
+      allPass
+        [ assertTrue "networkpolicy.yaml has app label" (isInfixOf lbl policy)
+        , assertTrue "daemonset.yaml has app label"    (isInfixOf lbl daemonset)
+        ]
+
+  , test "E2E: routes do not conflict with firewall deny rules" $ do
+      routes   <- readFileToString "configs/routes.ncl"
+      firewall <- readFileToString "configs/firewall.ncl"
+      allPass
+        [ assertTrue "firewall input_policy = DROP"
+            (isInfixOf "input_policy = \"DROP\"" firewall)
+        , assertTrue "firewall references ACTION_ACCEPT for ZT traffic"
+            (isInfixOf "ACTION_ACCEPT" firewall)
+        , assertTrue "routes has destination/target"
+            (isInfixOf "destination =" routes || isInfixOf "target =" routes)
+        ]
+
+  , test "E2E: secret manifest does not contain real credentials" $ do
+      content <- readFileToString "manifests/secret.yaml"
+      let hasPlaceholder = isInfixOf "EXAMPLE" content || isInfixOf "CHANGEME" content
+      let noKnownReal = not (isInfixOf "sk_live_" content)
+                     && not (isInfixOf "api_key=" content)
+      allPass
+        [ assertTrue "has EXAMPLE/CHANGEME placeholder" hasPlaceholder
+        , assertTrue "no Stripe/api_key= literal"       noKnownReal
+        ]
+
+  , test "E2E: network config IPv6 pool is valid format" $ do
+      content <- readFileToString "configs/network.ncl"
+      allPass
+        [ assertTrue "prefix = \" present"        (isInfixOf "prefix = \"" content)
+        , assertTrue "fd00:feed:face::/48 literal" (isInfixOf "fd00:feed:face::/48" content)
+        ]
+
+  , test "E2E: configmap provides auto-join configuration" $ do
+      content <- readFileToString "manifests/configmap.yaml"
+      allPass
+        [ assertTrue "kind: ConfigMap" (isInfixOf "kind: ConfigMap" content)
+        , assertTrue "data:"           (isInfixOf "data:" content)
+        ]
+
+  , test "E2E: daemonset includes health check configuration" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      let probe = isInfixOf "livenessProbe:" content
+               || isInfixOf "readinessProbe:" content
+      assertTrue "liveness or readiness probe present" probe
+
+  , test "E2E: all manifest references use existing configmap/secret" $ do
+      daemonset <- readFileToString "manifests/daemonset.yaml"
+      configmap <- readFileToString "manifests/configmap.yaml"
+      secret    <- readFileToString "manifests/secret.yaml"
+      allPass
+        [ assertTrue "daemonset -> zerotier-config"      (isInfixOf "zerotier-config" daemonset)
+        , assertTrue "daemonset -> zerotier-credentials" (isInfixOf "zerotier-credentials" daemonset)
+        , assertTrue "configmap defines zerotier-config" (isInfixOf "zerotier-config" configmap)
+        , assertTrue "secret defines zerotier-credentials" (isInfixOf "zerotier-credentials" secret)
+        ]
+
+  , test "E2E: firewall zones reference zerotier interface pattern" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      allPass
+        [ assertTrue "zerotier in firewall.ncl" (isInfixOf "zerotier" content)
+        , assertTrue "zt+ interface in firewall.ncl" (isInfixOf "zt+" content)
+        ]
+
+  , test "E2E: routes match network config IP pools" $ do
+      network <- readFileToString "configs/network.ncl"
+      routes  <- readFileToString "configs/routes.ncl"
+      allPass
+        [ assertTrue "network has IPv4 pool start" (isInfixOf "10.147.17.1" network)
+        , assertTrue "routes reference 10.147.17.0/24" (isInfixOf "10.147.17.0/24" routes)
+        ]
+
+  , test "E2E: capabilities in network config align with daemonset permissions" $ do
+      network   <- readFileToString "configs/network.ncl"
+      daemonset <- readFileToString "manifests/daemonset.yaml"
+      allPass
+        [ assertTrue "allow_managed_ips = true"
+            (isInfixOf "allow_managed_ips = true" network)
+        , assertTrue "NET_ADMIN capability in daemonset"
+            (isInfixOf "NET_ADMIN" daemonset)
+        ]
+  ]
diff --git a/tests/idris2/Main.idr b/tests/idris2/Main.idr
new file mode 100644
index 0000000..822bb32
--- /dev/null
+++ b/tests/idris2/Main.idr
@@ -0,0 +1,31 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+module Main
+
+import Test.Spec
+import UnitConfigStructureTest
+import ContractNetworkContractsTest
+import AspectSecurityTest
+import PropertyNetworkPropertyTest
+import SmokeInfraTest
+import E2ENetworkTest
+import System
+
+%default covering
+
+main : IO ()
+main = do
+  (p1, f1) <- runTestSuite "UnitConfigStructureTest" UnitConfigStructureTest.allSuites
+  (p2, f2) <- runTestSuite "ContractNetworkContractsTest" ContractNetworkContractsTest.allSuites
+  (p3, f3) <- runTestSuite "AspectSecurityTest" AspectSecurityTest.allSuites
+  (p4, f4) <- runTestSuite "PropertyNetworkPropertyTest" PropertyNetworkPropertyTest.allSuites
+  (p5, f5) <- runTestSuite "SmokeInfraTest" SmokeInfraTest.allSuites
+  (p6, f6) <- runTestSuite "E2ENetworkTest" E2ENetworkTest.allSuites
+  let totalPassed = p1 + p2 + p3 + p4 + p5 + p6
+  let totalFailed = f1 + f2 + f3 + f4 + f5 + f6
+  putStrLn ""
+  putStrLn $ "=== Total: " ++ show totalPassed ++ " passed, " ++ show totalFailed ++ " failed ==="
+  if totalFailed > 0
+    then exitWith (ExitFailure 1)
+    else pure ()
diff --git a/tests/idris2/PropertyNetworkPropertyTest.idr b/tests/idris2/PropertyNetworkPropertyTest.idr
new file mode 100644
index 0000000..411f554
--- /dev/null
+++ b/tests/idris2/PropertyNetworkPropertyTest.idr
@@ -0,0 +1,253 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Port of tests/property/network_property_test.ts to Idris2, estate-rollout 9/11.
+-- 11 of 11 property-style tests ported.
+--
+-- This file mixes content-validation (files exist + contain substrings) with
+-- pure-logic ports of the regex-driven property predicates: lowercase-hyphen
+-- filename validation, hex network-ID validation, dotted-quad IPv4 validation,
+-- IPv4-range ordering, CIDR-notation validation. Each predicate is exposed
+-- and unit-tested below so a regression in the predicate itself is caught
+-- alongside a regression in the file contents.
+
+module PropertyNetworkPropertyTest
+
+import Test.Spec
+import Data.String
+import Data.List
+import Data.Maybe
+import System.File
+
+%default covering
+
+-- File helpers ---------------------------------------------------------------
+
+readFileToString : String -> IO String
+readFileToString path = do
+  Right contents <- readFile path
+    | Left _ => pure ""
+  pure contents
+
+-- Pure helpers ---------------------------------------------------------------
+
+isLowerC : Char -> Bool
+isLowerC c = c >= 'a' && c <= 'z'
+
+isDigitC : Char -> Bool
+isDigitC c = c >= '0' && c <= '9'
+
+isHex : Char -> Bool
+isHex c =
+     isDigitC c
+  || (c >= 'a' && c <= 'f')
+  || (c >= 'A' && c <= 'F')
+
+-- Filename is /^[a-z-]+$/: at least 1 char, every char is a-z or '-'.
+public export
+isLowercaseHyphen : String -> Bool
+isLowercaseHyphen s =
+  let cs = unpack s in
+  length cs > 0 && all (\c => isLowerC c || c == '-') cs
+
+-- 16-character hex string: ZeroTier network ID format.
+public export
+isZTNetworkId : String -> Bool
+isZTNetworkId s =
+  let cs = unpack s in
+  length cs == 16 && all isHex cs
+
+-- Dotted-quad IPv4 parser.
+parseOctet : List Char -> Maybe (Nat, List Char)
+parseOctet xs =
+  let digits = takeWhile isDigitC xs
+      rest   = dropWhile isDigitC xs
+  in if length digits == 0 || length digits > 3
+       then Nothing
+       else case parsePositive (pack digits) of
+              Just n  => if n <= 255 then Just (n, rest) else Nothing
+              Nothing => Nothing
+
+public export
+parseIPv4 : String -> Maybe (Nat, Nat, Nat, Nat)
+parseIPv4 s =
+  let xs = unpack s in
+  case parseOctet xs of
+    Just (a, ('.' :: r1)) =>
+      case parseOctet r1 of
+        Just (b, ('.' :: r2)) =>
+          case parseOctet r2 of
+            Just (c, ('.' :: r3)) =>
+              case parseOctet r3 of
+                Just (d, []) => Just (a, b, c, d)
+                _            => Nothing
+            _ => Nothing
+        _ => Nothing
+    _ => Nothing
+
+public export
+ipv4ToNat : (Nat, Nat, Nat, Nat) -> Nat
+ipv4ToNat (a, b, c, d) =
+  a * 16777216 + b * 65536 + c * 256 + d
+
+-- A CIDR like "10.147.17.0/24" or "fd00:feed:face::/48". We accept either:
+--   - IPv4 dotted-quad + '/' + 1-2 digits
+--   - lowercase-hex with colons + '/' + 1-3 digits
+addrOkParsed : Maybe (Nat, Nat, Nat, Nat) -> List Char -> Bool
+addrOkParsed (Just _) _    = True
+addrOkParsed Nothing  addr = all (\c => isHex c || c == ':') addr
+
+public export
+addrOk : List Char -> Bool
+addrOk addr = addrOkParsed (parseIPv4 (pack addr)) addr
+
+checkCidrRest : List Char -> List Char -> Bool
+checkCidrRest addr (c :: rest) =
+  c == '/' && length addr > 0 && length rest > 0 && all isDigitC rest && addrOk addr
+checkCidrRest _ _ = False
+
+public export
+isCidr : String -> Bool
+isCidr s =
+  let parts = break (== '/') (unpack s) in
+  checkCidrRest (fst parts) (snd parts)
+
+-- Strip a known suffix from a String. Returns the prefix if it ends in
+-- `suf`, otherwise the original string.
+stripSuffix : String -> String -> String
+stripSuffix suf s =
+  let scs = unpack s
+      ucs = unpack suf
+  in if isSuffixOf ucs scs
+       then pack (take (length scs `minus` length ucs) scs)
+       else s
+
+public export
+allSuites : List TestCase
+allSuites =
+  [ test "Property: Nickel configs readable in 100-iteration loop" $ do
+      let loop : Nat -> IO Bool
+          loop Z     = pure True
+          loop (S k) = do
+            a <- readFileToString "configs/network.ncl"
+            b <- readFileToString "configs/firewall.ncl"
+            c <- readFileToString "configs/routes.ncl"
+            if length a > 0 && length b > 0 && length c > 0
+              then loop k
+              else pure False
+      ok <- loop 100
+      assertTrue "100 reads, all non-empty" ok
+
+  , test "Property: Nickel files follow lowercase-hyphen naming" $
+      allPass
+        [ assertTrue "network"  (isLowercaseHyphen (stripSuffix ".ncl" "network.ncl"))
+        , assertTrue "firewall" (isLowercaseHyphen (stripSuffix ".ncl" "firewall.ncl"))
+        , assertTrue "routes"   (isLowercaseHyphen (stripSuffix ".ncl" "routes.ncl"))
+        ]
+
+  , test "Property: Kubernetes manifest files follow naming conventions" $
+      allPass
+        [ assertTrue "configmap"      (isLowercaseHyphen (stripSuffix ".yaml" "configmap.yaml"))
+        , assertTrue "daemonset"      (isLowercaseHyphen (stripSuffix ".yaml" "daemonset.yaml"))
+        , assertTrue "namespace"      (isLowercaseHyphen (stripSuffix ".yaml" "namespace.yaml"))
+        , assertTrue "networkpolicy"  (isLowercaseHyphen (stripSuffix ".yaml" "networkpolicy.yaml"))
+        , assertTrue "secret"         (isLowercaseHyphen (stripSuffix ".yaml" "secret.yaml"))
+        , assertTrue "servicemonitor" (isLowercaseHyphen (stripSuffix ".yaml" "servicemonitor.yaml"))
+        ]
+
+  , test "Property: ZeroTier network ID format validation" $ do
+      -- Network ID is either a 16-char hex literal or a CHANGEME/EXAMPLE placeholder.
+      content <- readFileToString "configs/network.ncl"
+      let hasPlaceholderNetId =
+            isInfixOf "CHANGEME_NETWORK_ID" content
+            || isInfixOf "EXAMPLE_NETWORK_ID" content
+      -- Predicate sanity: 16-char hex passes, anything else fails.
+      allPass
+        [ assertTrue "predicate accepts 16-char hex"    (isZTNetworkId "0123456789abcdef")
+        , assertTrue "predicate rejects 15-char hex"    (not (isZTNetworkId "0123456789abcde"))
+        , assertTrue "predicate rejects non-hex chars"  (not (isZTNetworkId "01234567890zzzzz"))
+        , assertTrue "config has placeholder or 16-hex" hasPlaceholderNetId
+        ]
+
+  , test "Property: IPv4 assignment pool is valid range" $ do
+      -- Predicate sanity first.
+      let s = parseIPv4 "10.147.17.1"
+      let e = parseIPv4 "10.147.17.254"
+      let ordered = case (s, e) of
+                      (Just a, Just b) => ipv4ToNat a < ipv4ToNat b
+                      _                => False
+      -- Then confirm the config has the documented pool literals.
+      content <- readFileToString "configs/network.ncl"
+      allPass
+        [ assertTrue "start IPv4 parses"            (isJust s)
+        , assertTrue "end IPv4 parses"              (isJust e)
+        , assertTrue "start < end (Nat compare)"    ordered
+        , assertTrue "start literal in config"      (isInfixOf "10.147.17.1" content)
+        , assertTrue "end literal in config"        (isInfixOf "10.147.17.254" content)
+        ]
+
+  , test "Property: Firewall rules have action and type fields" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      let hasAction = isInfixOf "action =" content
+      let hasTypeOrProto = isInfixOf "type =" content || isInfixOf "protocol =" content
+      allPass
+        [ assertTrue "action field present" hasAction
+        , assertTrue "type or protocol field present" hasTypeOrProto
+        ]
+
+  , test "Property: Route destinations are valid CIDR notation" $ do
+      -- Predicate sanity.
+      allPass
+        [ assertTrue "10.147.17.0/24 is CIDR"          (isCidr "10.147.17.0/24")
+        , assertTrue "fd00:feed:face::/48 is CIDR"     (isCidr "fd00:feed:face::/48")
+        , assertTrue "192.168.1.1 (no prefix) rejected" (not (isCidr "192.168.1.1"))
+        , assertTrue "10.0.0.0/ (empty prefix) rejected" (not (isCidr "10.0.0.0/"))
+        ]
+
+  , test "Property: Route destination literals are CIDR" $ do
+      content <- readFileToString "configs/routes.ncl"
+      allPass
+        [ assertTrue "10.147.17.0/24 literal present"  (isInfixOf "10.147.17.0/24" content)
+        , assertTrue "fd00:feed:face::/48 literal present" (isInfixOf "fd00:feed:face::/48" content)
+        ]
+
+  , test "Property: Kubernetes manifest namespace consistency" $ do
+      d <- readFileToString "manifests/daemonset.yaml"
+      n <- readFileToString "manifests/networkpolicy.yaml"
+      s <- readFileToString "manifests/secret.yaml"
+      let ns = "zerotier-system"
+      allPass
+        [ assertTrue "daemonset.yaml -> zerotier-system"     (isInfixOf ("namespace: " ++ ns) d)
+        , assertTrue "networkpolicy.yaml -> zerotier-system" (isInfixOf ("namespace: " ++ ns) n)
+        , assertTrue "secret.yaml -> zerotier-system"        (isInfixOf ("namespace: " ++ ns) s)
+        ]
+
+  , test "Property: DaemonSet selector matches pod labels" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      allPass
+        [ assertTrue "has selector:"        (isInfixOf "selector:" content)
+        , assertTrue "has matchLabels:"     (isInfixOf "matchLabels:" content)
+        , assertTrue "selector mentions zerotier" (isInfixOf "zerotier" content)
+        ]
+
+  , test "Property: NetworkPolicy pod selector is defined" $ do
+      content <- readFileToString "manifests/networkpolicy.yaml"
+      allPass
+        [ assertTrue "podSelector:"  (isInfixOf "podSelector:" content)
+        , assertTrue "matchLabels:"  (isInfixOf "matchLabels:" content)
+        ]
+
+  , test "Property: Firewall zone names are valid identifiers" $ do
+      -- Predicate sanity: a few sample identifiers.
+      let isZoneName : String -> Bool
+          isZoneName s = let cs = unpack s in
+                         length cs > 0
+                      && all (\c => isLowerC c || isDigitC c || c == '_') cs
+      content <- readFileToString "configs/firewall.ncl"
+      allPass
+        [ assertTrue "zerotier is valid zone name"  (isZoneName "zerotier")
+        , assertTrue "Zerotier (capital) rejected"  (not (isZoneName "Zerotier"))
+        , assertTrue "zones = { in firewall.ncl"    (isInfixOf "zones = {" content)
+        , assertTrue "zerotier zone in firewall.ncl" (isInfixOf "zerotier =" content)
+        ]
+  ]
diff --git a/tests/idris2/SmokeInfraTest.idr b/tests/idris2/SmokeInfraTest.idr
new file mode 100644
index 0000000..5632f5e
--- /dev/null
+++ b/tests/idris2/SmokeInfraTest.idr
@@ -0,0 +1,119 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Port of tests/smoke/infra_smoke_test.ts to Idris2, estate-rollout 9/11.
+-- 9 of 9 smoke tests ported. All assertions are file-read + substring/prefix
+-- checks, so the Idris2 port is structurally identical to the Deno original.
+
+module SmokeInfraTest
+
+import Test.Spec
+import Data.String
+import System.File
+
+%default covering
+
+readFileToString : String -> IO String
+readFileToString path = do
+  Right contents <- readFile path
+    | Left _ => pure ""
+  pure contents
+
+-- Accept any of the three documented shebangs.
+hasBashShebang : String -> Bool
+hasBashShebang content =
+     isPrefixOf "#!/bin/bash"          content
+  || isPrefixOf "#!/bin/sh"            content
+  || isPrefixOf "#!/usr/bin/env bash"  content
+  || isPrefixOf "#!/usr/bin/env sh"    content
+
+public export
+allSuites : List TestCase
+allSuites =
+  [ test "Smoke: bash scripts exist with shebangs" $ do
+      a <- readFileToString "scripts/authorize-nodes.sh"
+      b <- readFileToString "scripts/configure-routes.sh"
+      c <- readFileToString "scripts/health-check.sh"
+      d <- readFileToString "scripts/join-network.sh"
+      allPass
+        [ assertTrue "authorize-nodes.sh"  (hasBashShebang a)
+        , assertTrue "configure-routes.sh" (hasBashShebang b)
+        , assertTrue "health-check.sh"     (hasBashShebang c)
+        , assertTrue "join-network.sh"     (hasBashShebang d)
+        ]
+
+  , test "Smoke: setup.sh exists with shell shebang" $ do
+      content <- readFileToString "setup.sh"
+      assertTrue "setup.sh shebang" (hasBashShebang content)
+
+  , test "Smoke: validation hooks exist with shell shebangs" $ do
+      a <- readFileToString "hooks/validate-codeql.sh"
+      b <- readFileToString "hooks/validate-permissions.sh"
+      c <- readFileToString "hooks/validate-sha-pins.sh"
+      d <- readFileToString "hooks/validate-spdx.sh"
+      allPass
+        [ assertTrue "validate-codeql.sh"      (hasBashShebang a)
+        , assertTrue "validate-permissions.sh" (hasBashShebang b)
+        , assertTrue "validate-sha-pins.sh"    (hasBashShebang c)
+        , assertTrue "validate-spdx.sh"        (hasBashShebang d)
+        ]
+
+  , test "Smoke: Idris2 ABI files exist and are non-empty" $ do
+      a <- readFileToString "src/abi/Layout.idr"
+      b <- readFileToString "src/abi/Types.idr"
+      c <- readFileToString "src/abi/Foreign.idr"
+      allPass
+        [ assertTrue "Layout.idr non-empty"  (length a > 0)
+        , assertTrue "Types.idr non-empty"   (length b > 0)
+        , assertTrue "Foreign.idr non-empty" (length c > 0)
+        ]
+
+  , test "Smoke: Kubernetes manifests are non-empty YAML" $ do
+      a <- readFileToString "manifests/configmap.yaml"
+      b <- readFileToString "manifests/daemonset.yaml"
+      c <- readFileToString "manifests/namespace.yaml"
+      d <- readFileToString "manifests/networkpolicy.yaml"
+      e <- readFileToString "manifests/secret.yaml"
+      f <- readFileToString "manifests/servicemonitor.yaml"
+      let hasYamlMeta : String -> Bool
+          hasYamlMeta = \s => isInfixOf "apiVersion:" s && isInfixOf "kind:" s
+      allPass
+        [ assertTrue "configmap.yaml"      (hasYamlMeta a)
+        , assertTrue "daemonset.yaml"      (hasYamlMeta b)
+        , assertTrue "namespace.yaml"      (hasYamlMeta c)
+        , assertTrue "networkpolicy.yaml"  (hasYamlMeta d)
+        , assertTrue "secret.yaml"         (hasYamlMeta e)
+        , assertTrue "servicemonitor.yaml" (hasYamlMeta f)
+        ]
+
+  , test "Smoke: manifests do not contain hardcoded secrets" $ do
+      a <- readFileToString "manifests/secret.yaml"
+      b <- readFileToString "manifests/daemonset.yaml"
+      -- Each file is either using EXAMPLE placeholders or *KeyRef references.
+      let ok : String -> Bool
+          ok = \s => isInfixOf "EXAMPLE" s
+                  || isInfixOf "secretKeyRef" s
+                  || isInfixOf "configMapKeyRef" s
+      allPass
+        [ assertTrue "secret.yaml uses placeholders or KeyRef"    (ok a)
+        , assertTrue "daemonset.yaml uses placeholders or KeyRef" (ok b)
+        ]
+
+  , test "Smoke: Idris2 Layout.idr has module declaration" $ do
+      content <- readFileToString "src/abi/Layout.idr"
+      assertTrue "module ZEROTIER_K8S_LINK.ABI.Layout"
+        (isInfixOf "module ZEROTIER_K8S_LINK.ABI.Layout" content)
+
+  , test "Smoke: Idris2 Types.idr has module declaration" $ do
+      content <- readFileToString "src/abi/Types.idr"
+      assertTrue "module ZEROTIER_K8S_LINK.ABI.Types"
+        (isInfixOf "module ZEROTIER_K8S_LINK.ABI.Types" content)
+
+  , test "Smoke: Idris2 Foreign.idr is non-empty" $ do
+      content <- readFileToString "src/abi/Foreign.idr"
+      assertTrue "Foreign.idr non-empty" (length content > 0)
+
+  , test "Smoke: root manifest file exists" $ do
+      content <- readFileToString "zerotier-k8s-link.manifest.ncl"
+      assertTrue "manifest non-empty" (length content > 0)
+  ]
diff --git a/tests/idris2/Test/Spec.idr b/tests/idris2/Test/Spec.idr
new file mode 100644
index 0000000..ff6a493
--- /dev/null
+++ b/tests/idris2/Test/Spec.idr
@@ -0,0 +1,112 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Minimal Idris2 test harness for the Gossamer ABI test suite.
+|||
+||| Mirrors the Deno.test interface used by the previous TypeScript suite:
+||| each test is a named IO action returning Bool (True = pass, False = fail).
+||| The runner reports per-test status and exits non-zero on any failure so
+||| Justfile / CI can detect breakage.
+
+module Test.Spec
+
+import Data.IORef
+import Data.List
+import System
+
+%default total
+
+public export
+record TestCase where
+  constructor MkTest
+  name : String
+  body : IO Bool
+
+public export
+test : String -> IO Bool -> TestCase
+test = MkTest
+
+||| Assert that two showable, comparable values are equal.
+||| Prints expected/actual on mismatch.
+public export
+assertEq : (Show a, Eq a) => a -> a -> IO Bool
+assertEq actual expected =
+  if actual == expected
+    then pure True
+    else do
+      putStrLn ""
+      putStrLn $ "  expected: " ++ show expected
+      putStrLn $ "  actual:   " ++ show actual
+      pure False
+
+||| Assert that two values are not equal.
+public export
+assertNotEq : (Show a, Eq a) => a -> a -> IO Bool
+assertNotEq actual notExpected =
+  if actual /= notExpected
+    then pure True
+    else do
+      putStrLn ""
+      putStrLn $ "  did not expect: " ++ show notExpected
+      pure False
+
+||| Assert that a Bool is True; print the supplied message on failure.
+public export
+assertTrue : String -> Bool -> IO Bool
+assertTrue msg b =
+  if b
+    then pure True
+    else do
+      putStrLn ""
+      putStrLn $ "  assertion failed: " ++ msg
+      pure False
+
+||| Combine a list of sub-assertions; all must pass.
+||| Use in a do-block to compose multiple checks in one test case.
+public export
+allPass : List (IO Bool) -> IO Bool
+allPass [] = pure True
+allPass (x :: xs) = do
+  r <- x
+  if r then allPass xs else pure False
+
+runOne : TestCase -> IO Bool
+runOne (MkTest name body) = do
+  putStr $ "  " ++ name ++ " ... "
+  result <- body
+  if result
+    then putStrLn "PASS"
+    else putStrLn "FAIL"
+  pure result
+
+runAll : List TestCase -> Nat -> Nat -> IO (Nat, Nat)
+runAll [] p f = pure (p, f)
+runAll (t :: ts) p f = do
+  ok <- runOne t
+  if ok
+    then runAll ts (S p) f
+    else runAll ts p (S f)
+
+||| Run a list of test cases. Reports a summary and exits non-zero
+||| if any test failed. Use for single-suite executables.
+public export
+runTests : List TestCase -> IO ()
+runTests cases = do
+  (p, f) <- runAll cases 0 0
+  putStrLn ""
+  putStrLn $ show p ++ " passed, " ++ show f ++ " failed"
+  if f > 0
+    then exitWith (ExitFailure 1)
+    else pure ()
+
+||| Run a named suite without exiting. Returns (passed, failed) so a parent
+||| aggregator (e.g. Main) can accumulate across multiple suites and only
+||| exit at the end.
+public export
+runTestSuite : String -> List TestCase -> IO (Nat, Nat)
+runTestSuite name cases = do
+  putStrLn $ "=== " ++ name ++ " ==="
+  (p, f) <- runAll cases 0 0
+  putStrLn $ show p ++ " passed, " ++ show f ++ " failed"
+  putStrLn ""
+  pure (p, f)
diff --git a/tests/idris2/UnitConfigStructureTest.idr b/tests/idris2/UnitConfigStructureTest.idr
new file mode 100644
index 0000000..80357b3
--- /dev/null
+++ b/tests/idris2/UnitConfigStructureTest.idr
@@ -0,0 +1,142 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Port of tests/unit/config_structure_test.ts to Idris2, estate-rollout port 9/11.
+-- 13 of 13 Deno.test cases ported. All assertions are file-read + substring
+-- matching, so the Idris2 port is structurally identical to the Deno original.
+
+module UnitConfigStructureTest
+
+import Test.Spec
+import Data.String
+import System.File
+
+%default covering
+
+readFileToString : String -> IO String
+readFileToString path = do
+  Right contents <- readFile path
+    | Left _ => pure ""
+  pure contents
+
+fileExists : String -> IO Bool
+fileExists path = do
+  Right _ <- readFile path
+    | Left _ => pure False
+  pure True
+
+nonEmptyFile : String -> IO Bool
+nonEmptyFile path = do
+  s <- readFileToString path
+  pure (length s > 0)
+
+public export
+allSuites : List TestCase
+allSuites =
+  [ test "Unit: Nickel config files exist" $ do
+      a <- nonEmptyFile "configs/network.ncl"
+      b <- nonEmptyFile "configs/firewall.ncl"
+      c <- nonEmptyFile "configs/routes.ncl"
+      assertTrue "all 3 Nickel config files non-empty" (a && b && c)
+
+  , test "Unit: Kubernetes manifest files exist" $ do
+      a <- nonEmptyFile "manifests/configmap.yaml"
+      b <- nonEmptyFile "manifests/daemonset.yaml"
+      c <- nonEmptyFile "manifests/namespace.yaml"
+      d <- nonEmptyFile "manifests/networkpolicy.yaml"
+      e <- nonEmptyFile "manifests/secret.yaml"
+      f <- nonEmptyFile "manifests/servicemonitor.yaml"
+      assertTrue "all 6 K8s manifest files non-empty"
+        (a && b && c && d && e && f)
+
+  , test "Unit: Nickel configs have SPDX headers" $ do
+      let spdx = "SPDX-License-Identifier: PMPL-1.0-or-later"
+      a <- readFileToString "configs/network.ncl"
+      b <- readFileToString "configs/firewall.ncl"
+      c <- readFileToString "configs/routes.ncl"
+      allPass
+        [ assertTrue "network.ncl SPDX"  (isInfixOf spdx a)
+        , assertTrue "firewall.ncl SPDX" (isInfixOf spdx b)
+        , assertTrue "routes.ncl SPDX"   (isInfixOf spdx c)
+        ]
+
+  , test "Unit: network.ncl contains ZeroTier config" $ do
+      content <- readFileToString "configs/network.ncl"
+      allPass
+        [ assertTrue "network_id"           (isInfixOf "network_id" content)
+        , assertTrue "api_token"            (isInfixOf "api_token" content)
+        , assertTrue "ipv4_assignment_pool" (isInfixOf "ipv4_assignment_pool" content)
+        , assertTrue "ipv6_assignment_pool" (isInfixOf "ipv6_assignment_pool" content)
+        , assertTrue "routes"               (isInfixOf "routes" content)
+        ]
+
+  , test "Unit: firewall.ncl contains firewall rules" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      allPass
+        [ assertTrue "rules"             (isInfixOf "rules" content)
+        , assertTrue "zerotier_control"  (isInfixOf "zerotier_control" content)
+        , assertTrue "established"       (isInfixOf "established" content)
+        , assertTrue "input_policy"      (isInfixOf "input_policy" content)
+        , assertTrue "forward_policy"    (isInfixOf "forward_policy" content)
+        , assertTrue "output_policy"     (isInfixOf "output_policy" content)
+        ]
+
+  , test "Unit: firewall.ncl has deny-by-default policy" $ do
+      content <- readFileToString "configs/firewall.ncl"
+      allPass
+        [ assertTrue "input_policy = DROP"   (isInfixOf "input_policy = \"DROP\"" content)
+        , assertTrue "forward_policy = DROP" (isInfixOf "forward_policy = \"DROP\"" content)
+        ]
+
+  , test "Unit: routes.ncl contains route definitions" $ do
+      content <- readFileToString "configs/routes.ncl"
+      allPass
+        [ assertTrue "static_routes"      (isInfixOf "static_routes" content)
+        , assertTrue "network_routes"     (isInfixOf "network_routes" content)
+        , assertTrue "10.147.17.0/24"     (isInfixOf "10.147.17.0/24" content)
+        , assertTrue "fd00:feed:face::/48" (isInfixOf "fd00:feed:face::/48" content)
+        ]
+
+  , test "Unit: daemonset.yaml references zerotier-system namespace" $ do
+      content <- readFileToString "manifests/daemonset.yaml"
+      allPass
+        [ assertTrue "namespace: zerotier-system" (isInfixOf "namespace: zerotier-system" content)
+        , assertTrue "kind: DaemonSet"            (isInfixOf "kind: DaemonSet" content)
+        , assertTrue "app.kubernetes.io/name: zerotier"
+            (isInfixOf "app.kubernetes.io/name: zerotier" content)
+        ]
+
+  , test "Unit: networkpolicy.yaml has ingress and egress rules" $ do
+      content <- readFileToString "manifests/networkpolicy.yaml"
+      allPass
+        [ assertTrue "kind: NetworkPolicy" (isInfixOf "kind: NetworkPolicy" content)
+        , assertTrue "ingress:"            (isInfixOf "ingress:" content)
+        , assertTrue "egress:"             (isInfixOf "egress:" content)
+        , assertTrue "policyTypes:"        (isInfixOf "policyTypes:" content)
+        , assertTrue "- Ingress"           (isInfixOf "- Ingress" content)
+        , assertTrue "- Egress"            (isInfixOf "- Egress" content)
+        ]
+
+  , test "Unit: secret.yaml has placeholder values only" $ do
+      content <- readFileToString "manifests/secret.yaml"
+      allPass
+        [ assertTrue "kind: Secret"                       (isInfixOf "kind: Secret" content)
+        , assertTrue "network-id: \"EXAMPLE_NETWORK_ID\"" (isInfixOf "network-id: \"EXAMPLE_NETWORK_ID\"" content)
+        , assertTrue "api-token: \"EXAMPLE_API_TOKEN\""   (isInfixOf "api-token: \"EXAMPLE_API_TOKEN\"" content)
+        ]
+
+  , test "Unit: namespace.yaml declares zerotier-system" $ do
+      content <- readFileToString "manifests/namespace.yaml"
+      allPass
+        [ assertTrue "kind: Namespace" (isInfixOf "kind: Namespace" content)
+        , assertTrue "zerotier-system" (isInfixOf "zerotier-system" content)
+        ]
+
+  , test "Unit: configmap.yaml is a ConfigMap" $ do
+      content <- readFileToString "manifests/configmap.yaml"
+      assertTrue "kind: ConfigMap" (isInfixOf "kind: ConfigMap" content)
+
+  , test "Unit: servicemonitor.yaml exists and is non-empty" $ do
+      ok <- nonEmptyFile "manifests/servicemonitor.yaml"
+      assertTrue "servicemonitor.yaml non-empty" ok
+  ]
diff --git a/zerotier-k8s-link-tests.ipkg b/zerotier-k8s-link-tests.ipkg
new file mode 100644
index 0000000..47554bb
--- /dev/null
+++ b/zerotier-k8s-link-tests.ipkg
@@ -0,0 +1,24 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- zerotier-k8s-link Idris2 test suite. Estate port 9/11 — all 6 TS test
+-- files ported (unit + contract + aspect + property + smoke + e2e),
+-- content-validation pattern with pure-logic ports for IPv4/CIDR/network-ID
+-- predicates.
+
+package zerotier-k8s-link-tests
+
+sourcedir = "tests/idris2"
+
+depends = base
+
+modules = Test.Spec
+        , UnitConfigStructureTest
+        , ContractNetworkContractsTest
+        , AspectSecurityTest
+        , PropertyNetworkPropertyTest
+        , SmokeInfraTest
+        , E2ENetworkTest
+        , Main
+
+main = Main
+
+executable = "zerotier-k8s-link-tests"