diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2d882642..f1dbc163 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -45,7 +45,7 @@ jobs:
           otp-version: "28"
 
       - name: Cache deps and _build
-        uses: actions/cache@v4
+        uses: actions/cache@v6
         with:
           path: |
             deps
@@ -55,7 +55,7 @@ jobs:
             ${{ runner.os }}-mix-${{ steps.beam.outputs.otp-version }}-${{ steps.beam.outputs.elixir-version }}-
 
       - name: Cache dialyzer PLTs
-        uses: actions/cache@v4
+        uses: actions/cache@v6
         with:
           path: priv/plts
           key: ${{ runner.os }}-plt-${{ steps.beam.outputs.otp-version }}-${{ steps.beam.outputs.elixir-version }}-${{ hashFiles('mix.lock') }}
@@ -97,7 +97,7 @@ jobs:
         run: mix coveralls.json --no-start --warnings-as-errors
 
       - name: Upload coverage to Codecov
-        uses: codecov/codecov-action@v5
+        uses: codecov/codecov-action@v7
         with:
           token: ${{ secrets.CODECOV_TOKEN }}
           files: cover/excoveralls.json
@@ -140,7 +140,7 @@ jobs:
         run: cargo llvm-cov --all-features --lcov --output-path lcov.info
 
       - name: Upload coverage to Codecov
-        uses: codecov/codecov-action@v5
+        uses: codecov/codecov-action@v7
         with:
           token: ${{ secrets.CODECOV_TOKEN }}
           # working-directory only applies to `run:` steps, not actions.
diff --git a/lib/hyper/suid_helper/dmsetup.ex b/lib/hyper/suid_helper/dmsetup.ex
index ee2452fd..aab579f9 100644
--- a/lib/hyper/suid_helper/dmsetup.ex
+++ b/lib/hyper/suid_helper/dmsetup.ex
@@ -18,9 +18,7 @@ defmodule Hyper.SuidHelper.Dmsetup do
           {:ok, Path.t()} | {:error, err()}
   @decorate with_span("Hyper.SuidHelper.Dmsetup.create_snapshot", include: [:name])
   def create_snapshot(name, origin_dev, cow_dev, sectors) do
-    table =
-      "0 #{sectors} snapshot #{origin_dev} #{cow_dev} P #{Hyper.Node.Config.Img.chunk_sectors()}"
-
+    table = snapshot_table(origin_dev, cow_dev, sectors, Hyper.Node.Config.Img.chunk_sectors())
     create(name, table, ["--readonly"])
   end
 
@@ -40,7 +38,7 @@ defmodule Hyper.SuidHelper.Dmsetup do
         ) :: {:ok, Path.t()} | {:error, err()}
   @decorate with_span("Hyper.SuidHelper.Dmsetup.create_thin_pool", include: [:name])
   def create_thin_pool(name, meta_dev, data_dev, sectors, block_sectors, low_water) do
-    table = "0 #{sectors} thin-pool #{meta_dev} #{data_dev} #{block_sectors} #{low_water}"
+    table = thin_pool_table(meta_dev, data_dev, sectors, block_sectors, low_water)
     create(name, table, [])
   end
 
@@ -53,7 +51,7 @@ defmodule Hyper.SuidHelper.Dmsetup do
           {:ok, Path.t()} | {:error, err()}
   @decorate with_span("Hyper.SuidHelper.Dmsetup.create_thin_external", include: [:name])
   def create_thin_external(name, pool_dev, dev_id, sectors, origin_dev) do
-    table = "0 #{sectors} thin #{pool_dev} #{dev_id} #{origin_dev}"
+    table = thin_external_table(pool_dev, dev_id, sectors, origin_dev)
     create(name, table, [])
   end
 
@@ -122,6 +120,25 @@ defmodule Hyper.SuidHelper.Dmsetup do
     |> MapSet.new()
   end
 
+  @doc false
+  @spec snapshot_table(Path.t(), Path.t(), pos_integer(), pos_integer()) :: String.t()
+  def snapshot_table(origin_dev, cow_dev, sectors, chunk_sectors) do
+    "0 #{sectors} snapshot #{origin_dev} #{cow_dev} P #{chunk_sectors}"
+  end
+
+  @doc false
+  @spec thin_pool_table(Path.t(), Path.t(), pos_integer(), pos_integer(), non_neg_integer()) ::
+          String.t()
+  def thin_pool_table(meta_dev, data_dev, sectors, block_sectors, low_water) do
+    "0 #{sectors} thin-pool #{meta_dev} #{data_dev} #{block_sectors} #{low_water}"
+  end
+
+  @doc false
+  @spec thin_external_table(Path.t(), non_neg_integer(), pos_integer(), Path.t()) :: String.t()
+  def thin_external_table(pool_dev, dev_id, sectors, origin_dev) do
+    "0 #{sectors} thin #{pool_dev} #{dev_id} #{origin_dev}"
+  end
+
   # Create a dm device named `name` from a reconstructed `table`, with any extra
   # create flags (e.g. `--readonly`). Returns the `/dev/mapper/<name>` path.
   @spec create(String.t(), String.t(), [String.t()]) :: {:ok, Path.t()} | {:error, err()}
diff --git a/lib/sys/linux/subid.ex b/lib/sys/linux/subid.ex
index eabc6390..9522d6d8 100644
--- a/lib/sys/linux/subid.ex
+++ b/lib/sys/linux/subid.ex
@@ -35,7 +35,7 @@ defmodule Sys.Linux.Subid do
       content
       |> String.split("\n", trim: true)
       |> Enum.reduce_while({:ok, []}, fn line, {:ok, acc} ->
-        case parse_subid_line(line) do
+        case parse(line) do
           {:ok, spec} -> {:cont, {:ok, [spec | acc]}}
           {:error, _} = error -> {:halt, error}
         end
@@ -43,8 +43,14 @@ defmodule Sys.Linux.Subid do
     end
   end
 
-  @spec parse_subid_line(String.t()) :: {:ok, Spec.t()} | {:error, :invalid_format}
-  defp parse_subid_line(line) do
+  @doc """
+  Parse one `/etc/subuid`/`/etc/subgid` line (`name:start:count`) into a `Spec`,
+  where `min_id` is `start` and `max_id` is `start + count`. A line that is not
+  exactly three colon-separated fields, or whose start/count are not integers,
+  yields `{:error, :invalid_format}`.
+  """
+  @spec parse(String.t()) :: {:ok, Spec.t()} | {:error, :invalid_format}
+  def parse(line) do
     with [name, start_str, count_str] <- String.split(line, ":"),
          {start, ""} <- Integer.parse(start_str),
          {count, ""} <- Integer.parse(count_str) do
diff --git a/mix.exs b/mix.exs
index e8ce13b5..7810a94b 100644
--- a/mix.exs
+++ b/mix.exs
@@ -56,6 +56,7 @@ defmodule Hyper.MixProject do
   defp deps do
     [
       {:credo, "~> 1.7", only: [:dev, :test], runtime: false},
+      {:stream_data, "~> 1.0", only: [:dev, :test], runtime: false},
       {:excoveralls, "~> 0.18", only: :test, runtime: false},
       {:dialyxir, "~> 1.4", only: [:dev], runtime: false},
       {:ex_doc, "~> 0.34", only: :dev, runtime: false},
diff --git a/mix.lock b/mix.lock
index e6794db5..0e682800 100644
--- a/mix.lock
+++ b/mix.lock
@@ -47,6 +47,7 @@
   "postgrex": {:hex, :postgrex, "0.22.2", "4aec14df2a72722aee92492566edbeeb44e233ecb86b1915d03136297ef1385d", [:mix], [{:db_connection, "~> 2.9", [hex: :db_connection, repo: "hexpm", optional: false]}, {:decimal, "~> 1.5 or ~> 2.0 or ~> 3.0", [hex: :decimal, repo: "hexpm", optional: false]}, {:jason, "~> 1.0", [hex: :jason, repo: "hexpm", optional: true]}, {:table, "~> 0.1.0", [hex: :table, repo: "hexpm", optional: true]}], "hexpm", "8946382ddb06294f56026ac4278b3cc212bac8a2c82ed68b4087819ed1abc53b"},
   "req": {:hex, :req, "0.6.2", "b9b2024f35bcf60a92cc8cad2eaaf9d4e7aace463ff74be1afe5986830184413", [:mix], [{:brotli, "~> 0.3.1", [hex: :brotli, repo: "hexpm", optional: true]}, {:ezstd, "~> 1.0", [hex: :ezstd, repo: "hexpm", optional: true]}, {:finch, "~> 0.21", [hex: :finch, repo: "hexpm", optional: false]}, {:jason, "~> 1.0", [hex: :jason, repo: "hexpm", optional: false]}, {:mime, "~> 2.0.6 or ~> 2.1", [hex: :mime, repo: "hexpm", optional: false]}, {:nimble_csv, "~> 1.0", [hex: :nimble_csv, repo: "hexpm", optional: true]}, {:plug, "~> 1.0", [hex: :plug, repo: "hexpm", optional: true]}], "hexpm", "cc9cd30a2ddd04989929b887178e1610c940456d962c6c3a52df6146d2eef9bf"},
   "ssl_verify_fun": {:hex, :ssl_verify_fun, "1.1.7", "354c321cf377240c7b8716899e182ce4890c5938111a1296add3ec74cf1715df", [:make, :mix, :rebar3], [], "hexpm", "fe4c190e8f37401d30167c8c405eda19469f34577987c76dde613e838bbc67f8"},
+  "stream_data": {:hex, :stream_data, "1.3.0", "bde37905530aff386dea1ddd86ecbf00e6642dc074ceffc10b7d4e41dfd6aac9", [:mix], [], "hexpm", "3cc552e286e817dca43c98044c706eec9318083a1480c52ae2688b08e2936e3c"},
   "telemetry": {:hex, :telemetry, "1.4.2", "a0cb522801dffb1c49fe6e30561badffc7b6d0e180db1300df759faa22062855", [:rebar3], [], "hexpm", "928f6495066506077862c0d1646609eed891a4326bee3126ba54b60af61febb1"},
   "telemetry_poller": {:hex, :telemetry_poller, "1.3.0", "d5c46420126b5ac2d72bc6580fb4f537d35e851cc0f8dbd571acf6d6e10f5ec7", [:rebar3], [{:telemetry, "~> 1.0", [hex: :telemetry, repo: "hexpm", optional: false]}], "hexpm", "51f18bed7128544a50f75897db9974436ea9bfba560420b646af27a9a9b35211"},
   "tls_certificate_check": {:hex, :tls_certificate_check, "1.33.0", "01e0822a2ebb0b207c4964e8d32ad8b1b8ce1caf58f446e53f816d06db953de4", [:rebar3], [{:ssl_verify_fun, "~> 1.1", [hex: :ssl_verify_fun, repo: "hexpm", optional: false]}], "hexpm", "cab9a7439e2dbfe91b38104f2d8a4b6d61dbc4d3a5ad59ac364713a88c6cfd9b"},
diff --git a/native/suidhelper/Cargo.lock b/native/suidhelper/Cargo.lock
index 8c12f9a2..86d964ac 100644
--- a/native/suidhelper/Cargo.lock
+++ b/native/suidhelper/Cargo.lock
@@ -52,6 +52,27 @@ dependencies = [
  "windows-sys",
 ]
 
+[[package]]
+name = "autocfg"
+version = "1.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53"
+
+[[package]]
+name = "bit-set"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "08807e080ed7f9d5433fa9b275196cfc35414f66a0c79d864dc51a0d825231a3"
+dependencies = [
+ "bit-vec",
+]
+
+[[package]]
+name = "bit-vec"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5e764a1d40d510daf35e07be9eb06e75770908c27d411ee6c92109c9840eaaf7"
+
 [[package]]
 name = "bitflags"
 version = "2.13.0"
@@ -122,6 +143,51 @@ version = "1.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
 
+[[package]]
+name = "errno"
+version = "0.3.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb"
+dependencies = [
+ "libc",
+ "windows-sys",
+]
+
+[[package]]
+name = "fastrand"
+version = "2.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6"
+
+[[package]]
+name = "fnv"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
+
+[[package]]
+name = "getrandom"
+version = "0.3.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "r-efi 5.3.0",
+ "wasip2",
+]
+
+[[package]]
+name = "getrandom"
+version = "0.4.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "300e883d756b2e4ec94e02791f39b04b522276138852cfc41d9fb7e904106099"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "r-efi 6.0.0",
+]
+
 [[package]]
 name = "hashbrown"
 version = "0.17.1"
@@ -140,6 +206,7 @@ version = "0.1.0"
 dependencies = [
  "clap",
  "nix",
+ "proptest",
  "serde",
  "serde_json",
  "thiserror",
@@ -174,6 +241,12 @@ version = "0.2.186"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
 
+[[package]]
+name = "linux-raw-sys"
+version = "0.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53"
+
 [[package]]
 name = "memchr"
 version = "2.8.2"
@@ -192,12 +265,36 @@ dependencies = [
  "libc",
 ]
 
+[[package]]
+name = "num-traits"
+version = "0.2.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841"
+dependencies = [
+ "autocfg",
+]
+
+[[package]]
+name = "once_cell"
+version = "1.21.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50"
+
 [[package]]
 name = "once_cell_polyfill"
 version = "1.70.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe"
 
+[[package]]
+name = "ppv-lite86"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9"
+dependencies = [
+ "zerocopy",
+]
+
 [[package]]
 name = "proc-macro2"
 version = "1.0.106"
@@ -207,6 +304,31 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "proptest"
+version = "1.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4b45fcc2344c680f5025fe57779faef368840d0bd1f42f216291f0dc4ace4744"
+dependencies = [
+ "bit-set",
+ "bit-vec",
+ "bitflags",
+ "num-traits",
+ "rand",
+ "rand_chacha",
+ "rand_xorshift",
+ "regex-syntax",
+ "rusty-fork",
+ "tempfile",
+ "unarray",
+]
+
+[[package]]
+name = "quick-error"
+version = "1.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0"
+
 [[package]]
 name = "quote"
 version = "1.0.45"
@@ -216,6 +338,87 @@ dependencies = [
  "proc-macro2",
 ]
 
+[[package]]
+name = "r-efi"
+version = "5.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f"
+
+[[package]]
+name = "r-efi"
+version = "6.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf"
+
+[[package]]
+name = "rand"
+version = "0.9.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea"
+dependencies = [
+ "rand_chacha",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb"
+dependencies = [
+ "ppv-lite86",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c"
+dependencies = [
+ "getrandom 0.3.4",
+]
+
+[[package]]
+name = "rand_xorshift"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "513962919efc330f829edb2535844d1b912b0fbe2ca165d613e4e8788bb05a5a"
+dependencies = [
+ "rand_core",
+]
+
+[[package]]
+name = "regex-syntax"
+version = "0.8.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4"
+
+[[package]]
+name = "rustix"
+version = "1.1.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b6fe4565b9518b83ef4f91bb47ce29620ca828bd32cb7e408f0062e9930ba190"
+dependencies = [
+ "bitflags",
+ "errno",
+ "libc",
+ "linux-raw-sys",
+ "windows-sys",
+]
+
+[[package]]
+name = "rusty-fork"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cc6bf79ff24e648f6da1f8d1f011e9cac26491b619e6b9280f2b47f1774e6ee2"
+dependencies = [
+ "fnv",
+ "quick-error",
+ "tempfile",
+ "wait-timeout",
+]
+
 [[package]]
 name = "serde"
 version = "1.0.228"
@@ -285,6 +488,19 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "tempfile"
+version = "3.27.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd"
+dependencies = [
+ "fastrand",
+ "getrandom 0.4.3",
+ "once_cell",
+ "rustix",
+ "windows-sys",
+]
+
 [[package]]
 name = "thiserror"
 version = "1.0.69"
@@ -339,6 +555,12 @@ dependencies = [
  "winnow",
 ]
 
+[[package]]
+name = "unarray"
+version = "0.1.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "eaea85b334db583fe3274d12b4cd1880032beab409c0d774be044d4480ab9a94"
+
 [[package]]
 name = "unicode-ident"
 version = "1.0.24"
@@ -351,6 +573,24 @@ version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
 
+[[package]]
+name = "wait-timeout"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "09ac3b126d3914f9849036f826e054cbabdc8519970b8998ddaf3b5bd3c65f11"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "wasip2"
+version = "1.0.4+wasi-0.2.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487"
+dependencies = [
+ "wit-bindgen",
+]
+
 [[package]]
 name = "windows-link"
 version = "0.2.1"
@@ -375,6 +615,32 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "wit-bindgen"
+version = "0.57.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.52"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ce1022995ff5ff5d841ad7d994facc23098cd40152f2c1d11cd607c6f530653f"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.52"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ae7f38b72ec2a254e2b87ef277cf2cd4fb97cbebf944faa6f33354da0867930"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "zmij"
 version = "1.0.21"
diff --git a/native/suidhelper/Cargo.toml b/native/suidhelper/Cargo.toml
index 0fe87c19..610cc429 100644
--- a/native/suidhelper/Cargo.toml
+++ b/native/suidhelper/Cargo.toml
@@ -8,6 +8,17 @@ description = "Tiny setuid-root helper that runs a whitelisted set of device com
 name = "hyper-suidhelper"
 path = "src/main.rs"
 
+# Integration tests mirror the `src/` module tree under `tests/`. Cargo only
+# auto-discovers test files at the top level of `tests/`, so each nested file
+# needs an explicit target pointing at its path.
+[[test]]
+name = "safe_path"
+path = "tests/util/safe_path.rs"
+
+[[test]]
+name = "safe_dev"
+path = "tests/util/safe_dev.rs"
+
 [dependencies]
 clap = { version = "4", features = ["derive"] }
 nix = { version = "0.29", features = ["user", "fs", "dir"] }
@@ -16,6 +27,9 @@ serde_json = "1"
 thiserror = "1"
 toml = { version = "0.8", default-features = false, features = ["parse"] }
 
+[dev-dependencies]
+proptest = "1"
+
 [profile.release]
 strip = true
 opt-level = "z"
diff --git a/native/suidhelper/src/lib.rs b/native/suidhelper/src/lib.rs
new file mode 100644
index 00000000..e34e9702
--- /dev/null
+++ b/native/suidhelper/src/lib.rs
@@ -0,0 +1,12 @@
+// `&'static str` const generics (`SafeBin<"losetup">`) are nightly-only.
+#![feature(adt_const_params)]
+#![feature(unsized_const_params)]
+#![allow(incomplete_features)]
+
+//! Library crate for the Hyper suidhelper. All logic lives here so it can be
+//! exercised by integration tests under `tests/`; `src/main.rs` is a thin entry
+//! point over these modules.
+
+pub mod config;
+pub mod tools;
+pub mod util;
diff --git a/native/suidhelper/src/main.rs b/native/suidhelper/src/main.rs
index 93bbb375..05732dde 100644
--- a/native/suidhelper/src/main.rs
+++ b/native/suidhelper/src/main.rs
@@ -1,21 +1,11 @@
-// `&'static str` const generics (`SafeBin<"losetup">`) are nightly-only.
-#![feature(adt_const_params)]
-#![feature(unsized_const_params)]
-#![allow(incomplete_features)]
-
-//! Tiny setuid-root helper for the unprivileged Hyper node.
-//!
-//! Hyper runs as a normal user but needs to attach loop devices and build
-//! device-mapper tables (losetup / dmsetup / blockdev), which require root. This
-//! helper is installed setuid root and exposes ONLY those operations, as a tree
-//! of typed subcommands (one per tool, see `src/tools`), each taking its `--bin`,
-//! plus a `sys-test` command to check installation.
+//! Tiny setuid-root helper for the unprivileged Hyper node — thin binary entry
+//! point. The privilege model and command tree live in the `hyper_suidhelper`
+//! library crate (`src/lib.rs`); this file only parses args and renders output.
 //!
 //! Privilege model: at startup we drop to the real uid; root is only ever held
 //! inside a `Privileged` scope (see `setuid_privileged`), which wraps just the
-//! tool's `run` (the `Command` call). Parsing the result happens after privileges
-//! are dropped. Each subcommand prints its result as JSON on stdout; errors go to
-//! stderr with a non-zero exit.
+//! tool's `run`. Each subcommand prints its result as JSON on stdout; errors go
+//! to stderr with a non-zero exit.
 //!
 //! Build & install:
 //!   cargo build --release
@@ -23,15 +13,12 @@
 //!     target/release/hyper-suidhelper /usr/local/bin/hyper-suidhelper
 //! Then: config :hyper, suid_helper: "/usr/local/bin/hyper-suidhelper"
 
-mod config;
-mod tools;
-mod util;
-
 use clap::{Parser, Subcommand};
+use hyper_suidhelper::config;
+use hyper_suidhelper::tools::Tool;
+use hyper_suidhelper::util::setuid_privileged::{self, Privileged};
 use serde::Serialize;
 use std::path::PathBuf;
-use tools::Tool;
-use util::setuid_privileged::{self, Privileged};
 
 #[derive(Parser)]
 #[command(
@@ -73,7 +60,7 @@ impl SysTest {
         Privileged::smoke_test()?;
         Ok(Self {
             sys_test: "ok",
-            hyper_base: crate::config::Config::get().hyper_base().to_path_buf(),
+            hyper_base: config::Config::get().hyper_base().to_path_buf(),
         })
     }
 }
diff --git a/native/suidhelper/src/util/safe_path.rs b/native/suidhelper/src/util/safe_path.rs
index f145aeaf..ed0cc051 100644
--- a/native/suidhelper/src/util/safe_path.rs
+++ b/native/suidhelper/src/util/safe_path.rs
@@ -48,11 +48,20 @@ impl Absoluteness for IsAbsolute {
 
 impl Components for StrictComponents {
     fn check(path: &Path) -> Result<(), ValidationError> {
-        // Only a leading root and plain names; `.`/`..`/prefix are rejected.
-        let ok = path
-            .components()
-            .all(|c| matches!(c, Component::RootDir | Component::Normal(_)));
-        if ok {
+        use std::os::unix::ffi::OsStrExt;
+
+        // `Path::components()` normalizes `.` and empty (`//`, trailing `/`)
+        // segments away before they can be inspected, so it cannot enforce the
+        // "no `.`/`..`/empty components" rule this gate documents. Validate the
+        // raw bytes instead (this is a Linux-only crate). The IsAbsolute axis
+        // guarantees the leading `/`; strip it, then require every `/`-separated
+        // segment to be a plain name: non-empty, and neither `.` nor `..` -- which
+        // is how the `..` traversal vector is rejected here.
+        let raw = path.as_os_str().as_bytes();
+        let body = raw.strip_prefix(b"/").unwrap_or(raw);
+
+        let is_plain_name = |seg: &[u8]| !seg.is_empty() && seg != b"." && seg != b"..";
+        if body.split(|&b| b == b'/').all(is_plain_name) {
             Ok(())
         } else {
             Err(ValidationError::LooseComponents)
diff --git a/native/suidhelper/tests/util/safe_dev.rs b/native/suidhelper/tests/util/safe_dev.rs
new file mode 100644
index 00000000..7dec4e2f
--- /dev/null
+++ b/native/suidhelper/tests/util/safe_dev.rs
@@ -0,0 +1,116 @@
+//! Property tests for the device/name validators — the lexical gate that keeps
+//! the privileged tools off arbitrary storage and blocks path tricks. Runs
+//! against the `hyper_suidhelper` library crate, not inline in source.
+
+use hyper_suidhelper::util::safe_dev::{BlockDev, DmName, LoopDev};
+use proptest::prelude::*;
+use std::path::Path;
+
+// The charset of a valid `hyper-*` dm name suffix: ascii-alphanumeric plus
+// `-`/`_`/`.`. Crucially excludes `/`, so a valid name can never traverse.
+fn name_suffix() -> impl Strategy<Value = String> {
+    "[a-zA-Z0-9._-]{0,16}"
+}
+
+proptest! {
+    // LoopDev accepts exactly `/dev/loop<digits>` and preserves the path.
+    #[test]
+    fn loopdev_accepts_dev_loop_n(n in any::<u64>()) {
+        let s = format!("/dev/loop{n}");
+        let dev = s.parse::<LoopDev>().unwrap();
+        prop_assert_eq!(dev.as_ref(), Path::new(&s));
+    }
+
+    // A `/dev/loop` whose suffix is empty or starts with a non-digit is never a
+    // valid loop device (covers `/dev/loop`, `/dev/loopX`, and path tricks whose
+    // first post-prefix byte is non-numeric).
+    #[test]
+    fn loopdev_rejects_non_numeric_suffix(suffix in "([^0-9].*)?") {
+        let s = format!("/dev/loop{suffix}");
+        prop_assert!(s.parse::<LoopDev>().is_err());
+    }
+
+    // A digit-led suffix that then contains any non-digit (e.g. `0/../sda`,
+    // `1a`, `2/x`) is rejected: is_loop requires the WHOLE suffix to be digits.
+    #[test]
+    fn loopdev_rejects_digit_then_junk(n in any::<u32>(), junk in "[^0-9].*") {
+        let s = format!("/dev/loop{n}{junk}");
+        prop_assert!(s.parse::<LoopDev>().is_err());
+    }
+
+    // BlockDev accepts a valid loop device.
+    #[test]
+    fn blockdev_accepts_loop(n in any::<u64>()) {
+        let s = format!("/dev/loop{n}");
+        prop_assert!(s.parse::<BlockDev>().is_ok());
+    }
+
+    // BlockDev accepts a valid `/dev/mapper/hyper-*` dm device.
+    #[test]
+    fn blockdev_accepts_hyper_dm(suffix in name_suffix()) {
+        let s = format!("/dev/mapper/hyper-{suffix}");
+        prop_assert!(s.parse::<BlockDev>().is_ok());
+    }
+
+    // BlockDev rejects a non-hyper dm device (e.g. `/dev/mapper/cryptroot`) —
+    // any mapper name not starting with `hyper-`.
+    #[test]
+    fn blockdev_rejects_non_hyper_dm(name in "[a-z][a-z0-9._-]{0,12}") {
+        prop_assume!(!name.starts_with("hyper-"));
+        let s = format!("/dev/mapper/{name}");
+        prop_assert!(s.parse::<BlockDev>().is_err());
+    }
+
+    // DmName accepts a `hyper-*` safe name and round-trips it through Display.
+    #[test]
+    fn dmname_accepts_hyper_name(suffix in name_suffix()) {
+        let s = format!("hyper-{suffix}");
+        let dm = s.parse::<DmName>().unwrap();
+        prop_assert_eq!(dm.to_string(), s);
+    }
+
+    // DmName rejects any name containing a `/` — the no-traversal guarantee.
+    #[test]
+    fn dmname_rejects_any_slash(pre in name_suffix(), post in name_suffix()) {
+        let s = format!("hyper-{pre}/{post}");
+        prop_assert!(s.parse::<DmName>().is_err());
+    }
+
+    // DmName rejects a name not starting with `hyper-`.
+    #[test]
+    fn dmname_rejects_non_hyper_prefix(s in "[a-zA-Z][a-zA-Z0-9._-]{0,12}") {
+        prop_assume!(!s.starts_with("hyper-"));
+        prop_assert!(s.parse::<DmName>().is_err());
+    }
+}
+
+// A curated set of concrete attack/edge strings that no generator is guaranteed
+// to hit, asserted explicitly. These are the cases the validators exist to stop.
+#[test]
+fn rejects_known_attack_strings() {
+    for bad in [
+        "/dev/loop",                     // empty number
+        "/dev/loop0/../sda",             // traversal off a loop dev
+        "/dev/loopX",                    // non-numeric
+        "/dev/sda",                      // arbitrary storage
+        "/dev/mapper/hyper-x/../../sda", // traversal via a hyper-looking name
+        "/dev/mapper/cryptroot",         // non-hyper dm
+        "../dev/loop0",                  // relative
+    ] {
+        assert!(bad.parse::<LoopDev>().is_err(), "LoopDev accepted {bad:?}");
+        assert!(
+            bad.parse::<BlockDev>().is_err(),
+            "BlockDev accepted {bad:?}"
+        );
+    }
+    for bad in [
+        "sda",
+        "hyper",
+        "nothyper-x",
+        "hyper-x/y",
+        "hyper-../x",
+        "/hyper-x",
+    ] {
+        assert!(bad.parse::<DmName>().is_err(), "DmName accepted {bad:?}");
+    }
+}
diff --git a/native/suidhelper/tests/util/safe_path.rs b/native/suidhelper/tests/util/safe_path.rs
new file mode 100644
index 00000000..908c256e
--- /dev/null
+++ b/native/suidhelper/tests/util/safe_path.rs
@@ -0,0 +1,131 @@
+//! Property tests for the lexical confinement gate. These run against the
+//! `hyper_suidhelper` library crate (Task 6's lib split), not inline in source.
+
+use hyper_suidhelper::util::safe_path::{IsAbsolute, SafePath, StrictComponents, ValidationError};
+use proptest::prelude::*;
+use std::path::PathBuf;
+
+// The fully-enforced flavor used at every real call site.
+type Strict = SafePath<IsAbsolute, StrictComponents>;
+
+// A plain, safe path component: no `.`/`..`/`/`/empty.
+fn safe_component() -> impl Strategy<Value = String> {
+    "[a-z][a-z0-9_]{0,7}"
+}
+
+// A component that must make StrictComponents reject the whole path.
+fn loose_component() -> impl Strategy<Value = String> {
+    prop_oneof![
+        Just(".".to_string()),
+        Just("..".to_string()),
+        Just("".to_string())
+    ]
+}
+
+fn join_abs(parts: &[String]) -> PathBuf {
+    let mut p = PathBuf::from("/");
+    for part in parts {
+        p.push(part);
+    }
+    p
+}
+
+proptest! {
+    // An absolute path of only plain components is always accepted.
+    #[test]
+    fn accepts_clean_absolute_paths(parts in prop::collection::vec(safe_component(), 1..6)) {
+        let path = join_abs(&parts);
+        prop_assert!(Strict::try_from(path).is_ok());
+    }
+
+    // A path containing ANY `.`/`..`/empty component is always rejected.
+    // (This is the confinement guarantee: `..`, `.`, and `//` never slip through.)
+    #[test]
+    fn rejects_any_loose_component(
+        prefix in prop::collection::vec(safe_component(), 0..4),
+        bad in loose_component(),
+        suffix in prop::collection::vec(safe_component(), 0..4),
+    ) {
+        let mut parts = prefix;
+        parts.push(bad);
+        parts.extend(suffix);
+        // Build the path from a RAW string, not via PathBuf::push: pushing an empty
+        // component collapses it to a bare separator, hiding the `//` we want to
+        // test. Raw joining makes `.`, `..`, and empty (`//`) literally present.
+        let path = PathBuf::from(format!("/{}", parts.join("/")));
+        prop_assert!(matches!(
+            Strict::try_from(path),
+            Err(ValidationError::LooseComponents)
+        ));
+    }
+
+    // A non-absolute path is always rejected on the absoluteness axis.
+    #[test]
+    fn rejects_relative_paths(parts in prop::collection::vec(safe_component(), 1..6)) {
+        let rel: PathBuf = parts.iter().collect();
+        prop_assert!(matches!(
+            Strict::try_from(rel),
+            Err(ValidationError::NotAbsolute)
+        ));
+    }
+
+    // relative_to reconstructs the original: base ++ parents ++ leaf == path.
+    #[test]
+    fn relative_to_round_trips(
+        base_parts in prop::collection::vec(safe_component(), 1..4),
+        rel_parts in prop::collection::vec(safe_component(), 1..5),
+    ) {
+        let base = join_abs(&base_parts);
+        let full_parts: Vec<String> =
+            base_parts.iter().chain(rel_parts.iter()).cloned().collect();
+        let full = join_abs(&full_parts);
+
+        let safe = Strict::try_from(full.clone()).unwrap();
+        let (parents, leaf) = safe.relative_to(&base).unwrap();
+
+        let mut rebuilt = base.clone();
+        for p in &parents {
+            rebuilt.push(p);
+        }
+        rebuilt.push(&leaf);
+        prop_assert_eq!(rebuilt, full);
+
+        // The decomposed pieces are exactly the relative components.
+        let mut decomposed: Vec<String> =
+            parents.iter().map(|p| p.to_string_lossy().into_owned()).collect();
+        decomposed.push(leaf.to_string_lossy().into_owned());
+        prop_assert_eq!(decomposed, rel_parts);
+    }
+
+    // A path that is not under `base` is rejected, never silently decomposed.
+    #[test]
+    fn relative_to_rejects_paths_outside_base(
+        base_parts in prop::collection::vec(safe_component(), 1..4),
+        other_parts in prop::collection::vec(safe_component(), 1..4),
+    ) {
+        // Force divergence at the first component so `other` cannot be under `base`.
+        let base = join_abs(&base_parts);
+        let mut other = vec!["zzdifferent".to_string()];
+        other.extend(other_parts);
+        let path = join_abs(&other);
+
+        let safe = Strict::try_from(path).unwrap();
+        prop_assert!(matches!(
+            safe.relative_to(&base),
+            Err(ValidationError::NotUnderBase)
+        ));
+    }
+
+    // A path equal to the base has no leaf component.
+    #[test]
+    fn relative_to_base_itself_has_no_leaf(
+        base_parts in prop::collection::vec(safe_component(), 1..4),
+    ) {
+        let base = join_abs(&base_parts);
+        let safe = Strict::try_from(base.clone()).unwrap();
+        prop_assert!(matches!(
+            safe.relative_to(&base),
+            Err(ValidationError::NoLeaf)
+        ));
+    }
+}
diff --git a/test/controls/ewma_properties_test.exs b/test/controls/ewma_properties_test.exs
new file mode 100644
index 00000000..591e0f6a
--- /dev/null
+++ b/test/controls/ewma_properties_test.exs
@@ -0,0 +1,61 @@
+defmodule Controls.EwmaPropertiesTest do
+  @moduledoc """
+  Invariants of the first-order EWMA filter that hold for any tau, any positive
+  dt, and any sample sequence. Because alpha is strictly in (0, 1), the filter is
+  a convex blend: its output can never overshoot past either endpoint. The first
+  sample seeds the filter exactly, and a unit-quantity sample keeps its unit.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Controls.Ewma
+  alias Unit.Information
+
+  defp tau, do: integer(1..100_000)
+  defp dt, do: integer(1..100_000)
+  defp num, do: one_of([integer(-1_000_000..1_000_000), float(min: -1.0e6, max: 1.0e6)])
+
+  property "the first sample seeds the value exactly, regardless of dt" do
+    check all(t <- tau(), x <- num(), d <- dt()) do
+      assert Ewma.value(Ewma.update(Ewma.new(t), x, d)) == x
+    end
+  end
+
+  property "after one update the value stays within [min(prev, sample), max(prev, sample)]" do
+    check all(t <- tau(), prev <- num(), sample <- num(), d <- dt()) do
+      e = Ewma.new(t) |> Ewma.update(prev, d) |> Ewma.update(sample, d)
+      v = Ewma.value(e)
+      lo = min(prev, sample)
+      hi = max(prev, sample)
+      # Inclusive bounds with a tiny epsilon for float round-off at the endpoints.
+      assert v >= lo - 1.0e-6
+      assert v <= hi + 1.0e-6
+    end
+  end
+
+  property "feeding the current value back in is a fixed point" do
+    check all(t <- tau(), x <- num(), d <- dt()) do
+      e = Ewma.new(t) |> Ewma.update(x, d) |> Ewma.update(x, d)
+      assert_in_delta Ewma.value(e), x, 1.0e-6
+    end
+  end
+
+  property "a unit-quantity sample is filtered and comes back as the same unit" do
+    check all(
+            t <- tau(),
+            prev_b <- integer(0..1_000_000),
+            sample_b <- integer(0..1_000_000),
+            d <- dt()
+          ) do
+      e =
+        Ewma.new(t)
+        |> Ewma.update(Information.bytes(prev_b), d)
+        |> Ewma.update(Information.bytes(sample_b), d)
+
+      assert %Information{} = Ewma.value(e)
+      bytes = Information.as_bytes(Ewma.value(e))
+      assert bytes >= min(prev_b, sample_b)
+      assert bytes <= max(prev_b, sample_b)
+    end
+  end
+end
diff --git a/test/controls/rate_properties_test.exs b/test/controls/rate_properties_test.exs
new file mode 100644
index 00000000..0bc13093
--- /dev/null
+++ b/test/controls/rate_properties_test.exs
@@ -0,0 +1,80 @@
+defmodule Controls.RatePropertiesTest do
+  @moduledoc """
+  `Controls.Rate.compute/3` is a pure state machine. These properties pin every
+  branch: the three conditions that must yield `:skip` (re-baselining without
+  emitting a meaningless rate), and the arithmetic of the one `:ok` branch.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Controls.Rate
+
+  defp count, do: integer(0..1_000_000_000)
+  defp mono, do: integer(-1_000_000..1_000_000)
+
+  property "the first observation (nil state) always skips and seeds the baseline" do
+    check all(c <- count(), t <- mono()) do
+      assert Rate.compute(nil, c, t) == {:skip, {c, t}}
+    end
+  end
+
+  property "a counter that went backwards skips and re-baselines to the new reading" do
+    # A counter that can regress is necessarily >= 1, so prev_c starts at 1; this
+    # also keeps the `drop` range (1..prev_c) non-empty. StreamData RAISES on an
+    # empty range rather than re-generating, so an empty draw would crash the property.
+    check all(
+            prev_c <- integer(1..1_000_000_000),
+            prev_t <- mono(),
+            drop <- integer(1..prev_c),
+            t <- mono()
+          ) do
+      c = prev_c - drop
+      assert c < prev_c
+      assert Rate.compute({prev_c, prev_t}, c, t) == {:skip, {c, t}}
+    end
+  end
+
+  property "a non-positive dt skips (no division by a stale or reversed clock)" do
+    check all(
+            prev_c <- count(),
+            prev_t <- mono(),
+            extra <- count(),
+            back <- integer(0..1_000_000)
+          ) do
+      c = prev_c + extra
+      t = prev_t - back
+      assert t <= prev_t
+      assert Rate.compute({prev_c, prev_t}, c, t) == {:skip, {c, t}}
+    end
+  end
+
+  property "a forward counter over positive dt yields the exact non-negative rate" do
+    check all(
+            prev_c <- count(),
+            prev_t <- mono(),
+            gain <- count(),
+            dt <- integer(1..1_000_000)
+          ) do
+      c = prev_c + gain
+      t = prev_t + dt
+      assert {:ok, rate, {^c, ^t}} = Rate.compute({prev_c, prev_t}, c, t)
+      assert rate == gain * 1000.0 / dt
+      assert rate >= 0.0
+    end
+  end
+
+  property "at a fixed dt, a larger counter delta never produces a smaller rate" do
+    check all(
+            prev_c <- count(),
+            prev_t <- mono(),
+            g1 <- count(),
+            g2 <- count(),
+            dt <- integer(1..1_000_000)
+          ) do
+      t = prev_t + dt
+      {:ok, r1, _} = Rate.compute({prev_c, prev_t}, prev_c + g1, t)
+      {:ok, r2, _} = Rate.compute({prev_c, prev_t}, prev_c + g2, t)
+      if g1 <= g2, do: assert(r1 <= r2), else: assert(r1 >= r2)
+    end
+  end
+end
diff --git a/test/hyper/suid_helper/dmsetup_properties_test.exs b/test/hyper/suid_helper/dmsetup_properties_test.exs
new file mode 100644
index 00000000..73858fc6
--- /dev/null
+++ b/test/hyper/suid_helper/dmsetup_properties_test.exs
@@ -0,0 +1,76 @@
+defmodule Hyper.SuidHelper.DmsetupPropertiesTest do
+  @moduledoc """
+  Pins the device-mapper table grammar produced by the pure builders: a table
+  always begins at sector 0, names the right target, and places every field in
+  its kernel-mandated position. A reordered or mis-positioned field would map
+  the wrong device, so each property splits the table back into fields and
+  asserts positions. Also covers `parse_targets/1` round-trip.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Hyper.SuidHelper.Dmsetup
+
+  # A device path / token with no whitespace (whitespace is the field separator).
+  defp dev, do: string([?a..?z, ?A..?Z, ?0..?9, ?/, ?-, ?_, ?.], min_length: 1, max_length: 16)
+  defp pos, do: integer(1..1_000_000_000)
+  defp nonneg, do: integer(0..1_000_000_000)
+
+  property "snapshot_table places origin, cow, persistent flag, and chunk in order" do
+    check all(origin <- dev(), cow <- dev(), sectors <- pos(), chunk <- pos()) do
+      table = Dmsetup.snapshot_table(origin, cow, sectors, chunk)
+
+      assert ["0", s, "snapshot", o, c, "P", ch] = String.split(table)
+      assert s == "#{sectors}"
+      assert o == origin
+      assert c == cow
+      assert ch == "#{chunk}"
+    end
+  end
+
+  property "thin_pool_table places meta, data, block size, and low water in order" do
+    check all(meta <- dev(), data <- dev(), sectors <- pos(), block <- pos(), low <- nonneg()) do
+      table = Dmsetup.thin_pool_table(meta, data, sectors, block, low)
+
+      assert ["0", s, "thin-pool", m, d, b, w] = String.split(table)
+      assert s == "#{sectors}"
+      assert m == meta
+      assert d == data
+      assert b == "#{block}"
+      assert w == "#{low}"
+    end
+  end
+
+  property "thin_external_table places pool, dev_id, and origin in order" do
+    check all(pool <- dev(), dev_id <- nonneg(), sectors <- pos(), origin <- dev()) do
+      table = Dmsetup.thin_external_table(pool, dev_id, sectors, origin)
+
+      assert ["0", s, "thin", p, id, o] = String.split(table)
+      assert s == "#{sectors}"
+      assert p == pool
+      assert id == "#{dev_id}"
+      assert o == origin
+    end
+  end
+
+  property "every table starts at logical sector 0 and a positive length" do
+    check all(origin <- dev(), cow <- dev(), sectors <- pos(), chunk <- pos()) do
+      table = Dmsetup.snapshot_table(origin, cow, sectors, chunk)
+      assert ["0", len | _] = String.split(table)
+      assert String.to_integer(len) == sectors
+      assert sectors > 0
+    end
+  end
+
+  property "parse_targets recovers the first column of each non-blank line" do
+    check all(targets <- uniq_list_of(dev(), min_length: 1, max_length: 6)) do
+      # Render each as a `dmsetup targets` row: "<name> vM.m.p" plus blank lines.
+      out =
+        targets
+        |> Enum.map_join("\n", fn t -> "#{t}        v1.2.3" end)
+        |> Kernel.<>("\n\n")
+
+      assert Dmsetup.parse_targets(out) == MapSet.new(targets)
+    end
+  end
+end
diff --git a/test/sys/linux/cgroup/v2_properties_test.exs b/test/sys/linux/cgroup/v2_properties_test.exs
new file mode 100644
index 00000000..cc185905
--- /dev/null
+++ b/test/sys/linux/cgroup/v2_properties_test.exs
@@ -0,0 +1,62 @@
+defmodule Sys.Linux.Cgroup.V2PropertiesTest do
+  @moduledoc """
+  Invariants of the pure cgroup-v2 config builder and its `as_linux/1` renderer:
+  each setter is reflected in exactly its interface file, the rendered strings
+  match the kernel's `cpu.max`/`memory.max` formats, and an empty config renders
+  to an empty map.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Sys.Linux.Cgroup.V2.Config
+
+  defp pos, do: integer(1..1_000_000_000)
+
+  property "an empty config renders to an empty map" do
+    assert Config.as_linux(Config.new()) == %{}
+  end
+
+  property "cpu_max renders quota and period under the cpu.max key" do
+    check all(quota <- pos(), period <- pos()) do
+      linux = Config.new() |> Config.cpu_max(quota, period) |> Config.as_linux()
+      assert linux == %{"cpu.max": "#{quota} #{period}"}
+    end
+  end
+
+  property "memory_max renders as the byte string under :\"memory.max\"" do
+    check all(bytes <- pos()) do
+      linux = Config.new() |> Config.memory_max(bytes) |> Config.as_linux()
+      assert linux == %{"memory.max": "#{bytes}"}
+    end
+  end
+
+  property "both limits render independently, regardless of set order" do
+    check all(quota <- pos(), period <- pos(), bytes <- pos()) do
+      a = Config.new() |> Config.cpu_max(quota, period) |> Config.memory_max(bytes)
+      b = Config.new() |> Config.memory_max(bytes) |> Config.cpu_max(quota, period)
+
+      expected = %{"cpu.max": "#{quota} #{period}", "memory.max": "#{bytes}"}
+      assert Config.as_linux(a) == expected
+      assert Config.as_linux(b) == expected
+    end
+  end
+
+  property "the last write to a key wins" do
+    check all(q1 <- pos(), p1 <- pos(), q2 <- pos(), p2 <- pos()) do
+      linux =
+        Config.new()
+        |> Config.cpu_max(q1, p1)
+        |> Config.cpu_max(q2, p2)
+        |> Config.as_linux()
+
+      assert linux == %{"cpu.max": "#{q2} #{p2}"}
+    end
+  end
+
+  property "the last memory_max write wins" do
+    check all(b1 <- pos(), b2 <- pos()) do
+      linux = Config.new() |> Config.memory_max(b1) |> Config.memory_max(b2) |> Config.as_linux()
+      assert linux == %{"memory.max": "#{b2}"}
+    end
+  end
+end
diff --git a/test/sys/linux/fstab_properties_test.exs b/test/sys/linux/fstab_properties_test.exs
new file mode 100644
index 00000000..9fef631a
--- /dev/null
+++ b/test/sys/linux/fstab_properties_test.exs
@@ -0,0 +1,76 @@
+defmodule Sys.Linux.FstabPropertiesTest do
+  @moduledoc """
+  Generative round-trip for fstab lines: render a well-formed entry from random
+  fields, parse it, and assert every field is recovered (options comma-split,
+  the dump/pass columns ignored). Plus the structural rules: comments and blank
+  lines are rejected, and a line with fewer than four fields is invalid.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Sys.Linux.Fstab
+
+  # A single fstab token: no whitespace, no comma (commas separate options),
+  # non-empty. Restricting to a safe charset keeps rendered lines unambiguous.
+  defp token, do: string([?a..?z, ?A..?Z, ?0..?9, ?/, ?-, ?_, ?.], min_length: 1, max_length: 12)
+  defp opts, do: list_of(token(), min_length: 1, max_length: 5)
+
+  property "round-trips device, mount_point, fs_type, and comma-split options" do
+    check all(
+            device <- token(),
+            mount_point <- token(),
+            fs_type <- token(),
+            mount_opts <- opts()
+          ) do
+      line = "#{device} #{mount_point} #{fs_type} #{Enum.join(mount_opts, ",")}"
+      assert {:ok, spec} = Fstab.parse(line)
+      assert spec.device == device
+      assert spec.mount_point == mount_point
+      assert spec.fs_type == fs_type
+      assert spec.mount_opts == mount_opts
+    end
+  end
+
+  property "the dump and pass columns are ignored" do
+    check all(
+            device <- token(),
+            mount_point <- token(),
+            fs_type <- token(),
+            mount_opts <- opts(),
+            dump <- integer(0..9),
+            pass <- integer(0..9)
+          ) do
+      line = "#{device} #{mount_point} #{fs_type} #{Enum.join(mount_opts, ",")} #{dump} #{pass}"
+      assert {:ok, spec} = Fstab.parse(line)
+      assert spec.device == device
+      assert spec.mount_opts == mount_opts
+    end
+  end
+
+  property "extra leading/trailing whitespace does not change the parse" do
+    check all(device <- token(), mount_point <- token(), fs_type <- token(), o <- token()) do
+      line = "   #{device}   #{mount_point}  #{fs_type}   #{o}   "
+      assert {:ok, spec} = Fstab.parse(line)
+      assert spec.device == device
+      assert spec.mount_point == mount_point
+      assert spec.fs_type == fs_type
+      assert spec.mount_opts == [o]
+    end
+  end
+
+  property "comment and blank lines are rejected" do
+    check all(
+            ws <- string([?\s, ?\t], max_length: 4),
+            rest <- string(:printable, max_length: 20)
+          ) do
+      assert Fstab.parse(ws) == {:error, :invalid_format}
+      assert Fstab.parse("#" <> rest) == {:error, :invalid_format}
+    end
+  end
+
+  property "a line with fewer than four fields is invalid" do
+    check all(fields <- list_of(token(), min_length: 0, max_length: 3)) do
+      assert Fstab.parse(Enum.join(fields, " ")) == {:error, :invalid_format}
+    end
+  end
+end
diff --git a/test/sys/linux/proc/counter_parser_properties_test.exs b/test/sys/linux/proc/counter_parser_properties_test.exs
new file mode 100644
index 00000000..df169939
--- /dev/null
+++ b/test/sys/linux/proc/counter_parser_properties_test.exs
@@ -0,0 +1,115 @@
+defmodule Sys.Linux.Proc.CounterParserPropertiesTest do
+  @moduledoc """
+  Generative round-trips for the three counter-oriented /proc parsers. Each builds
+  a syntactically valid file from random counters and asserts the parser recovers
+  them, applies the right column offsets and unit conversions, and drops the header
+  and malformed rows.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Sys.Linux.Proc.{Diskstats, Meminfo, NetDev}
+  alias Unit.Information
+
+  defp big, do: integer(0..1_000_000_000_000)
+  # An interface/device name: lowercase letters/digits, optionally with a `:alias`.
+  defp ifname do
+    gen all(
+          base <- string([?a..?z, ?0..?9], min_length: 1, max_length: 6),
+          alias_suffix <- one_of([constant(""), map(integer(0..9), &":#{&1}")])
+        ) do
+      base <> alias_suffix
+    end
+  end
+
+  describe "NetDev.parse/1" do
+    property "round-trips rx (col 0) and tx (col 8), keeps alias names, drops headers" do
+      check all(
+              rows <-
+                uniq_list_of(
+                  gen(
+                    all name <- ifname(), counters <- list_of(big(), length: 16) do
+                      {name, counters}
+                    end
+                  ),
+                  uniq_fun: fn {n, _} -> n end,
+                  min_length: 1,
+                  max_length: 6
+                )
+            ) do
+        body =
+          Enum.map_join(rows, "\n", fn {name, c} ->
+            "  #{name}: " <> Enum.map_join(c, " ", &Integer.to_string/1)
+          end)
+
+        content = "Inter-|   Receive ...\n face |bytes ... |bytes ...\n" <> body
+        parsed = NetDev.parse(content)
+
+        assert length(parsed) == length(rows)
+
+        for {name, c} <- rows do
+          iface = Enum.find(parsed, &(&1.name == name))
+          assert iface.rx_bytes == Enum.at(c, 0)
+          assert iface.tx_bytes == Enum.at(c, 8)
+        end
+      end
+    end
+  end
+
+  describe "Diskstats.parse/1" do
+    property "converts sectors (idx 5/9) to bytes via x512 and round-trips names" do
+      check all(
+              rows <-
+                uniq_list_of(
+                  gen(
+                    all name <- ifname(),
+                        major <- integer(0..259),
+                        minor <- integer(0..255),
+                        stats <- list_of(big(), length: 14) do
+                      {name, major, minor, stats}
+                    end
+                  ),
+                  uniq_fun: fn {n, _, _, _} -> n end,
+                  min_length: 1,
+                  max_length: 6
+                )
+            ) do
+        body =
+          Enum.map_join(rows, "\n", fn {name, maj, min, stats} ->
+            "  #{maj}  #{min} #{name} " <> Enum.map_join(stats, " ", &Integer.to_string/1)
+          end)
+
+        parsed = Diskstats.parse(body)
+        assert length(parsed) == length(rows)
+
+        for {name, _maj, _min, stats} <- rows do
+          dev = Enum.find(parsed, &(&1.name == name))
+          assert dev.read_bytes == Enum.at(stats, 2) * 512
+          assert dev.write_bytes == Enum.at(stats, 6) * 512
+        end
+      end
+    end
+  end
+
+  describe "Meminfo.parse/1" do
+    property "wraps each kB value as Information (bytes = kB x 1024)" do
+      check all(total <- big(), avail <- big(), free <- big(), buffers <- big(), cached <- big()) do
+        content = """
+        MemTotal:       #{total} kB
+        MemFree:        #{free} kB
+        MemAvailable:   #{avail} kB
+        Buffers:        #{buffers} kB
+        Cached:         #{cached} kB
+        SwapTotal:      0 kB
+        """
+
+        snap = Meminfo.parse(content)
+        assert Information.as_bytes(snap.total) == total * 1024
+        assert Information.as_bytes(snap.available) == avail * 1024
+        assert Information.as_bytes(snap.free) == free * 1024
+        assert Information.as_bytes(snap.buffers) == buffers * 1024
+        assert Information.as_bytes(snap.cached) == cached * 1024
+      end
+    end
+  end
+end
diff --git a/test/sys/linux/proc/stat_properties_test.exs b/test/sys/linux/proc/stat_properties_test.exs
new file mode 100644
index 00000000..c447bc11
--- /dev/null
+++ b/test/sys/linux/proc/stat_properties_test.exs
@@ -0,0 +1,110 @@
+defmodule Sys.Linux.Proc.StatPropertiesTest do
+  @moduledoc """
+  Generative round-trip for `/proc/stat`: build a syntactically valid file from
+  random counters, parse it, and assert every value survived. Also pins the
+  `CpuTimes` arithmetic (total = sum of all ten states; idle = idle + iowait) and
+  the kernel-compat rule that missing trailing columns default to zero.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Sys.Linux.Proc.Stat
+  alias Sys.Linux.Proc.Stat.CpuTimes
+
+  defp counter, do: integer(0..1_000_000_000)
+  # A full 10-column CPU line's worth of jiffies.
+  defp cpu_cols, do: list_of(counter(), length: 10)
+  defp cpu_line(prefix, cols), do: Enum.join([prefix | Enum.map(cols, &Integer.to_string/1)], " ")
+
+  property "CpuTimes.from_columns round-trips all ten state counters" do
+    check all(cols <- cpu_cols()) do
+      t = CpuTimes.from_columns(cols)
+
+      assert [
+               t.user,
+               t.nice,
+               t.system,
+               t.idle,
+               t.iowait,
+               t.irq,
+               t.softirq,
+               t.steal,
+               t.guest,
+               t.guest_nice
+             ] == cols
+    end
+  end
+
+  property "total is the sum of all states and idle is idle + iowait" do
+    check all(cols <- cpu_cols()) do
+      t = CpuTimes.from_columns(cols)
+      assert CpuTimes.total(t) == Enum.sum(cols)
+      assert CpuTimes.idle(t) == Enum.at(cols, 3) + Enum.at(cols, 4)
+    end
+  end
+
+  property "missing trailing columns default to zero (older-kernel compatibility)" do
+    check all(n <- integer(3..9), cols <- list_of(counter(), length: n)) do
+      t = CpuTimes.from_columns(cols)
+
+      present = [
+        t.user,
+        t.nice,
+        t.system,
+        t.idle,
+        t.iowait,
+        t.irq,
+        t.softirq,
+        t.steal,
+        t.guest,
+        t.guest_nice
+      ]
+
+      assert Enum.take(present, n) == cols
+      assert Enum.drop(present, n) |> Enum.all?(&(&1 == 0))
+    end
+  end
+
+  property "a synthesized /proc/stat round-trips the aggregate, per-core, and scalar fields" do
+    check all(
+            agg <- cpu_cols(),
+            cores <- list_of(cpu_cols(), min_length: 1, max_length: 8),
+            ctxt <- counter(),
+            btime <- counter(),
+            processes <- counter(),
+            running <- counter(),
+            blocked <- counter()
+          ) do
+      core_lines =
+        cores
+        |> Enum.with_index()
+        |> Enum.map(fn {cols, i} -> cpu_line("cpu#{i}", cols) end)
+
+      content =
+        ([cpu_line("cpu", agg)] ++
+           core_lines ++
+           [
+             # An intr line with a long body the parser must skip regardless of length.
+             "intr 999 1 2 3 4 5 6 7 8 9 10 11 12",
+             "ctxt #{ctxt}",
+             "btime #{btime}",
+             "processes #{processes}",
+             "procs_running #{running}",
+             "procs_blocked #{blocked}",
+             "softirq 123 4 5 6 7"
+           ])
+        |> Enum.join("\n")
+
+      snap = Stat.parse(content)
+
+      assert CpuTimes.total(snap.cpu) == Enum.sum(agg)
+      assert length(snap.cpus) == length(cores)
+      assert Enum.map(snap.cpus, &CpuTimes.total/1) == Enum.map(cores, &Enum.sum/1)
+      assert snap.ctxt == ctxt
+      assert snap.btime == btime
+      assert snap.processes == processes
+      assert snap.procs_running == running
+      assert snap.procs_blocked == blocked
+    end
+  end
+end
diff --git a/test/sys/linux/subid_properties_test.exs b/test/sys/linux/subid_properties_test.exs
new file mode 100644
index 00000000..80d70e30
--- /dev/null
+++ b/test/sys/linux/subid_properties_test.exs
@@ -0,0 +1,45 @@
+defmodule Sys.Linux.SubidPropertiesTest do
+  @moduledoc """
+  Invariants of `Subid.parse/1`: a well-formed `name:start:count` round-trips to
+  a range whose width is exactly `count` (max_id = start + count), and malformed
+  lines (wrong field count, non-integer fields) are rejected.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Sys.Linux.Subid
+
+  # A subuid name: no colon (the field separator), non-empty.
+  defp name, do: string([?a..?z, ?A..?Z, ?0..?9, ?_, ?-], min_length: 1, max_length: 12)
+  defp nonneg, do: integer(0..4_000_000_000)
+  # A token guaranteed NOT to be a bare integer (letters only), for malformed cases.
+  defp alpha, do: string([?a..?z, ?A..?Z], min_length: 1, max_length: 8)
+
+  property "round-trips name/start and makes max_id = start + count" do
+    check all(n <- name(), start <- nonneg(), count <- nonneg()) do
+      assert {:ok, spec} = Subid.parse("#{n}:#{start}:#{count}")
+      assert spec.name == n
+      assert spec.min_id == start
+      assert spec.max_id == start + count
+      assert spec.max_id - spec.min_id == count
+      assert spec.max_id >= spec.min_id
+    end
+  end
+
+  property "a line without exactly three colon fields is invalid" do
+    check all(
+            fields <- list_of(name(), min_length: 0, max_length: 5),
+            fields != [] and length(fields) != 3
+          ) do
+      assert Subid.parse(Enum.join(fields, ":")) == {:error, :invalid_format}
+    end
+  end
+
+  property "non-integer start or count is rejected" do
+    check all(n <- name(), junk <- alpha(), start <- nonneg()) do
+      # `junk` is letters only, so it can never be a bare integer string.
+      assert Subid.parse("#{n}:#{junk}:5") == {:error, :invalid_format}
+      assert Subid.parse("#{n}:#{start}:#{junk}") == {:error, :invalid_format}
+    end
+  end
+end
diff --git a/test/unit/quantity_properties_test.exs b/test/unit/quantity_properties_test.exs
new file mode 100644
index 00000000..90174095
--- /dev/null
+++ b/test/unit/quantity_properties_test.exs
@@ -0,0 +1,104 @@
+defmodule Unit.QuantityPropertiesTest do
+  @moduledoc """
+  Laws that must hold for EVERY `Unit.Quantity` value, generated across all three
+  dimensions. The quantities are a signed additive group (commutative, associative,
+  zero identity, subtraction is the inverse) with a total order that mirrors the
+  backing integer scalar exactly. These are the contracts `Unit.Operators` and the
+  `Unit.Quantity` protocol promise; the example tests only spot-check them.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+  use Unit.Operators
+
+  alias Unit.{Bandwidth, Information, Quantity, Time}
+
+  # A bounded scalar keeps generated magnitudes readable in shrink output; Elixir
+  # integers are bignums so there is no overflow concern, the bound is purely for
+  # legible counterexamples.
+  defp scalar, do: integer(-1_000_000..1_000_000)
+
+  # One generator per dimension: a random scalar wrapped through the canonical
+  # (bytes / bytes-per-sec / nanosecond) constructor.
+  defp quantity do
+    one_of([
+      map(scalar(), &Information.bytes/1),
+      map(scalar(), &Bandwidth.bps/1),
+      map(scalar(), &Time.ns/1)
+    ])
+  end
+
+  # A pair of quantities guaranteed to share a dimension (so `+`/`-`/ordering are
+  # defined). Built by generating two scalars and one dimension constructor.
+  defp same_dim_pair do
+    gen all(
+          ctor <- member_of([&Information.bytes/1, &Bandwidth.bps/1, &Time.ns/1]),
+          a <- scalar(),
+          b <- scalar()
+        ) do
+      {ctor.(a), ctor.(b)}
+    end
+  end
+
+  property "with_value/value is a round-trip in both directions" do
+    check all(q <- quantity(), n <- scalar()) do
+      assert Quantity.value(Quantity.with_value(q, n)) == n
+      assert Quantity.with_value(q, Quantity.value(q)) == q
+    end
+  end
+
+  property "addition mirrors integer addition on the scalar" do
+    check all({a, b} <- same_dim_pair()) do
+      assert Quantity.value(a + b) == Quantity.value(a) + Quantity.value(b)
+    end
+  end
+
+  property "addition is commutative and associative" do
+    check all(
+            ctor <- member_of([&Information.bytes/1, &Bandwidth.bps/1, &Time.ns/1]),
+            x <- scalar(),
+            y <- scalar(),
+            z <- scalar()
+          ) do
+      a = ctor.(x)
+      b = ctor.(y)
+      c = ctor.(z)
+      assert a + b == b + a
+      assert a + (b + c) == a + b + c
+    end
+  end
+
+  property "zero is the additive identity and subtraction is the inverse" do
+    check all({a, b} <- same_dim_pair()) do
+      zero = Quantity.with_value(a, 0)
+      assert zero + a == a
+      # `a - a` is exactly the subtraction-inverse law under test; the "always 0"
+      # warning is the point here, not a mistake.
+      # credo:disable-for-next-line Credo.Check.Warning.OperationOnSameValues
+      assert a - a == zero
+      assert a + b - b == a
+    end
+  end
+
+  property "ordering matches the integer order of the backing scalars" do
+    check all({a, b} <- same_dim_pair()) do
+      assert a < b == Quantity.value(a) < Quantity.value(b)
+      assert a <= b == Quantity.value(a) <= Quantity.value(b)
+      assert a > b == Quantity.value(a) > Quantity.value(b)
+      assert a <= b or b <= a
+    end
+  end
+
+  property "mixing two different dimensions always raises ArgumentError" do
+    pairs = [
+      {Information.bytes(1), Time.ns(1)},
+      {Time.ns(1), Bandwidth.bps(1)},
+      {Bandwidth.bps(1), Information.bytes(1)}
+    ]
+
+    check all({a, b} <- member_of(pairs)) do
+      assert_raise ArgumentError, fn -> a + b end
+      assert_raise ArgumentError, fn -> a - b end
+      assert_raise ArgumentError, fn -> a < b end
+    end
+  end
+end