diff --git a/bench/utils/unlink/Makefile b/bench/utils/unlink/Makefile
new file mode 100644
index 00000000..6bf21a50
--- /dev/null
+++ b/bench/utils/unlink/Makefile
@@ -0,0 +1,14 @@
+PROJECT_DIR := $(abspath $(dir $(lastword $(MAKEFILE_LIST))))
+REPO_ROOT := $(abspath $(PROJECT_DIR)/../../..)
+LOCAL_TASK := $(notdir $(PROJECT_DIR))
+
+.PHONY: build verify test
+
+build:
+	python3 -m benchmarks.make_tasks build --root "$(REPO_ROOT)" --task "$(LOCAL_TASK)"
+
+verify:
+	python3 -m benchmarks.verify --project "$(PROJECT_DIR)" --library "$(PROJECT_DIR)/../../core"
+
+test:
+	python3 -m benchmarks.make_tasks test --root "$(REPO_ROOT)" --task "$(LOCAL_TASK)"
diff --git a/bench/utils/unlink/Tests.dfy b/bench/utils/unlink/Tests.dfy
new file mode 100644
index 00000000..a82be3b8
--- /dev/null
+++ b/bench/utils/unlink/Tests.dfy
@@ -0,0 +1,25 @@
+include "UnlinkSchema.dfy"
+
+module UnlinkTests {
+  import S = UnlinkSchema
+  import C = CliTypes
+
+  // Ordinary operands select execution mode and retain their pathname.
+  method {:test} TestOrdinaryOperand() {
+    var parsed := C.ParsedArgs("unlink", [], ["target"], false);
+    var raw := S.Decode(parsed);
+    expect raw.mode == S.ModeRun;
+    expect raw.operands == ["target"];
+  }
+
+  // Help preceding version selects help mode.
+  method {:test} TestHelpBeforeVersion() {
+    var parsed := C.ParsedArgs("unlink", [
+      C.OptOccurrence("unlink.help", C.Long("help"), C.None, 0, "--help"),
+      C.OptOccurrence("unlink.version", C.Long("version"), C.None, 1, "--version")
+    ], [], false);
+    var raw := S.Decode(parsed);
+    expect raw.mode == S.ModeHelp;
+  }
+
+}
diff --git a/bench/utils/unlink/Tests.py b/bench/utils/unlink/Tests.py
new file mode 100644
index 00000000..c9c44ac6
--- /dev/null
+++ b/bench/utils/unlink/Tests.py
@@ -0,0 +1,370 @@
+"""GNU parity cases for unlink."""
+
+from pathlib import Path
+
+import pytest
+
+from tools.bench.bench_test_support import (
+    assert_result_matches_reference,
+    bench_dll_path,
+    build_bench_utility,
+    build_coreutils_utility,
+    coreutils_binary_path,
+    evaluation_target_root,
+    run_bench_utility,
+    run_coreutils_utility,
+    run_dafny_verify,
+)
+
+ROOT = evaluation_target_root(Path(__file__).resolve().parents[3])
+UTILITY = "unlink"
+PROJECT = ROOT / "bench" / "utils" / UTILITY
+
+
+@pytest.fixture(scope="session")
+def executables() -> tuple[Path, Path]:
+    """Build the two targets only for runtime cases; local Make targets use -n0."""
+    build_bench_utility(ROOT, UTILITY)
+    build_coreutils_utility(ROOT, UTILITY)
+    return (
+        coreutils_binary_path(ROOT, ROOT / "_build/coreutils/src" / UTILITY),
+        bench_dll_path(ROOT, ROOT / "_build/bench" / f"{UTILITY}_bench.dll"),
+    )
+
+
+def assert_parity(
+    executables: tuple[Path, Path],
+    args: list[str],
+    cwd: Path,
+) -> None:
+    """Compare a read-only scenario, including stderr on error exits."""
+    reference, candidate = executables
+    expected = run_coreutils_utility(reference, UTILITY, args, cwd)
+    actual = run_bench_utility(candidate, args, cwd)
+    assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False)
+
+
+# Missing operands report a failure and usage guidance.
+def test_missing_operand_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: none - Adds missing-operand parity.
+    # upstream-reason: parity.
+    assert_parity(executables, [], tmp_path)
+
+
+# Extra operands are rejected without deleting either file.
+def test_extra_operand_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: none - Adds extra-operand parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    (ref_dir / "a").write_bytes(b"hello a")
+    (bench_dir / "a").write_bytes(b"hello a")
+    (ref_dir / "b").write_bytes(b"hello b")
+    (bench_dir / "b").write_bytes(b"hello b")
+
+    reference, candidate = executables
+    ref = run_coreutils_utility(reference, UTILITY, ["a", "b"], ref_dir)
+    bench = run_bench_utility(candidate, ["a", "b"], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+
+    for dir in (ref_dir, bench_dir):
+        assert (dir / "a").read_bytes() == b"hello a"
+        assert (dir / "b").read_bytes() == b"hello b"
+
+
+# Extra-operand diagnostics quote special characters without removing either file.
+@pytest.mark.parametrize("operand", ["a'b", 'a"b', "a\nb", "a\tb", "a\\b", "a b"])
+def test_quoted_extra_operand_matches_coreutils(
+    executables: tuple[Path, Path], tmp_path: Path, operand: str
+) -> None:
+    # upstream: none - Regression for the extra-operand quoting mismatch.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    for directory in (ref_dir, bench_dir):
+        directory.mkdir()
+        (directory / "target").write_bytes(b"keep target")
+        (directory / operand).write_bytes(b"keep extra operand")
+
+    reference, candidate = executables
+    expected = run_coreutils_utility(reference, UTILITY, ["target", operand], ref_dir)
+    actual = run_bench_utility(candidate, ["target", operand], bench_dir)
+    assert_result_matches_reference(expected, actual, ignore_stderr_when_exit_nonzero=False)
+    assert expected[2] == actual[2] == 1
+    for directory in (ref_dir, bench_dir):
+        assert (directory / "target").read_bytes() == b"keep target"
+        assert (directory / operand).read_bytes() == b"keep extra operand"
+
+
+# Failed unlink diagnostics use GNU path quoting for special characters.
+@pytest.mark.parametrize("operand", ["a'b", 'a"b', "a\nb", "a\tb", "a\\b", "a b"])
+def test_quoted_missing_path_matches_coreutils(
+    executables: tuple[Path, Path], tmp_path: Path, operand: str
+) -> None:
+    # upstream: none - Regression for literal paths in deletion diagnostics.
+    # upstream-reason: parity.
+    assert_parity(executables, [operand], tmp_path)
+
+
+# The unlink_setup ordinary-execution case removes a regular file's name.
+def test_regular_file_deletion_matches_coreutils(
+    executables: tuple[Path, Path], tmp_path: Path
+) -> None:
+    # upstream: coreutils/tests/help/help-version.sh
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    (ref_dir / "target").write_bytes(b"2147483647 0\n")
+    (bench_dir / "target").write_bytes(b"2147483647 0\n")
+
+    reference, candidate = executables
+    ref = run_coreutils_utility(reference, UTILITY, ["target"], ref_dir)
+    bench = run_bench_utility(candidate, ["target"], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+
+    assert not (ref_dir / "target").exists()
+    assert not (bench_dir / "target").exists()
+
+
+# Deleting a symbolic link preserves its target.
+def test_symlink_deletion_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: none - Adds symlink deletion parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    reference, candidate = executables
+
+    for dir in (ref_dir, bench_dir):
+        (dir / "target").write_bytes(b"hello")
+        (dir / "link").symlink_to("target")
+
+    ref = run_coreutils_utility(reference, UTILITY, ["link"], ref_dir)
+    bench = run_bench_utility(candidate, ["link"], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+    assert ref[2] == bench[2] == 0
+
+    for dir in (ref_dir, bench_dir):
+        assert not (dir / "link").is_symlink()
+        assert (dir / "target").read_bytes() == b"hello"
+
+
+# A dangling symbolic link can be removed.
+def test_dangling_symlink_deletion_matches_coreutils(
+    executables: tuple[Path, Path], tmp_path: Path
+) -> None:
+    # upstream: none - Adds dangling-symlink parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    reference, candidate = executables
+
+    for dir in (ref_dir, bench_dir):
+        (dir / "target").write_bytes(b"hello")
+        (dir / "link").symlink_to("target")
+        (dir / "target").unlink()
+
+    ref = run_coreutils_utility(reference, UTILITY, ["link"], ref_dir)
+    bench = run_bench_utility(candidate, ["link"], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+    assert ref[2] == bench[2] == 0
+
+    for dir in (ref_dir, bench_dir):
+        assert not (dir / "link").is_symlink()
+        assert not (dir / "target").exists()
+
+
+# Deleting one hard-link name preserves the other name.
+def test_hard_link_deletion_matches_coreutils(
+    executables: tuple[Path, Path], tmp_path: Path
+) -> None:
+    # upstream: none - Adds hard-link deletion parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    reference, candidate = executables
+
+    for dir in (ref_dir, bench_dir):
+        (dir / "target").write_bytes(b"hello")
+        (dir / "alias").hardlink_to(dir / "target")
+
+    ref = run_coreutils_utility(reference, UTILITY, ["alias"], ref_dir)
+    bench = run_bench_utility(candidate, ["alias"], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+    assert ref[2] == bench[2] == 0
+
+    for dir in (ref_dir, bench_dir):
+        assert not (dir / "alias").exists()
+        assert (dir / "target").read_bytes() == b"hello"
+        assert (dir / "target").stat().st_nlink == 1
+
+
+# A nonexistent pathname produces a deletion error.
+def test_missing_path_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: none - Adds missing-path parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    reference, candidate = executables
+
+    ref = run_coreutils_utility(reference, UTILITY, ["nothing"], ref_dir)
+    bench = run_bench_utility(candidate, ["nothing"], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+    assert ref[2] == bench[2] == 1
+
+
+# An empty pathname produces a deletion error.
+def test_empty_path_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: none - Adds empty-path parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    reference, candidate = executables
+
+    ref = run_coreutils_utility(reference, UTILITY, [""], ref_dir)
+    bench = run_bench_utility(candidate, [""], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+    assert ref[2] == bench[2] == 1
+
+
+# A directory operand is rejected without deleting its contents.
+def test_directory_operand_matches_coreutils(
+    executables: tuple[Path, Path], tmp_path: Path
+) -> None:
+    # upstream: none - Adds directory rejection parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    for dir in (ref_dir, bench_dir):
+        (dir / "folder").mkdir()
+        (dir / "folder" / "target").write_bytes(b"hello")
+    reference, candidate = executables
+
+    ref = run_coreutils_utility(reference, UTILITY, ["folder"], ref_dir)
+    bench = run_bench_utility(candidate, ["folder"], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+    assert ref[2] == bench[2] == 1
+    for dir in (ref_dir, bench_dir):
+        assert (dir / "folder").is_dir()
+        assert (dir / "folder" / "target").read_bytes() == b"hello"
+
+
+# Help exits successfully with the GNU help output.
+def test_help_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: coreutils/tests/help/help-version.sh
+    assert_parity(executables, ["--help"], tmp_path)
+
+
+# Version exits successfully with the GNU version output.
+def test_version_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: coreutils/tests/help/help-version.sh
+    assert_parity(executables, ["--version"], tmp_path)
+
+
+# An unknown long option produces the diagnostic checked by GNU's option test.
+def test_invalid_option_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: coreutils/tests/misc/usage_vs_getopt.sh
+    assert_parity(executables, ["--thisoptiondoesnotexist"], tmp_path)
+
+
+# Help and version respect GNU option precedence.
+def test_option_precedence_matches_coreutils(
+    executables: tuple[Path, Path], tmp_path: Path
+) -> None:
+    # upstream: none - Adds mixed-option precedence parity.
+    # upstream-reason: parity.
+    for args in [
+        ["--help", "--version"],
+        ["--version", "--help"],
+        ["--help", "--bad"],
+        ["--bad", "--help"],
+    ]:
+        assert_parity(executables, args, tmp_path)
+
+
+# GNU's BEFORE/AFTER cases keep help and version ahead of file operands.
+def test_help_version_with_operands_matches_coreutils(
+    executables: tuple[Path, Path], tmp_path: Path
+) -> None:
+    # upstream: coreutils/tests/help/help-version-getopt.sh
+    reference, candidate = executables
+    for option in ("--help", "--version"):
+        expected = run_coreutils_utility(reference, UTILITY, [option], tmp_path)
+        assert expected[2] == 0
+        for args in (
+            [option, "AFTER"],
+            ["BEFORE", option],
+            ["BEFORE", option, "AFTER"],
+        ):
+            actual_reference = run_coreutils_utility(reference, UTILITY, args, tmp_path)
+            actual_candidate = run_bench_utility(candidate, args, tmp_path)
+            assert actual_reference == expected
+            assert_result_matches_reference(actual_reference, actual_candidate)
+
+
+# The option delimiter permits a pathname beginning with a hyphen.
+def test_option_like_path_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: none - Adds unlink-specific -- delimiter parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    reference, candidate = executables
+    (ref_dir / "--help").write_bytes(b"hello")
+    (bench_dir / "--help").write_bytes(b"hello")
+
+    ref = run_coreutils_utility(reference, UTILITY, ["--", "--help"], ref_dir)
+    bench = run_bench_utility(candidate, ["--", "--help"], bench_dir)
+    assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+    assert ref[2] == bench[2] == 0
+    for dir in (ref_dir, bench_dir):
+        assert not (dir / "--help").exists()
+
+
+# A non-writable parent directory prevents deletion and preserves the file.
+def test_no_permission_matches_coreutils(executables: tuple[Path, Path], tmp_path: Path) -> None:
+    # upstream: none - Adds permission-denied parity.
+    # upstream-reason: parity.
+    ref_dir = tmp_path / "reference"
+    bench_dir = tmp_path / "candidate"
+    ref_dir.mkdir()
+    bench_dir.mkdir()
+    try:
+        for dir in (ref_dir, bench_dir):
+            (dir / "target").write_bytes(b"hello")
+            dir.chmod(0o555)
+        reference, candidate = executables
+
+        ref = run_coreutils_utility(reference, UTILITY, ["target"], ref_dir)
+        bench = run_bench_utility(candidate, ["target"], bench_dir)
+        assert_result_matches_reference(ref, bench, ignore_stderr_when_exit_nonzero=False)
+        assert ref[2] == bench[2] == 1
+        for dir in (ref_dir, bench_dir):
+            assert (dir / "target").read_bytes() == b"hello"
+    finally:
+        ref_dir.chmod(0o755)
+        bench_dir.chmod(0o755)
+
+
+# Check each proof module as well as the entry contract required by make check.
+@pytest.mark.dafny_verify
+@pytest.mark.parametrize("filename", ["UnlinkCore.dfy", "UnlinkProof.dfy", "Unlink.dfy"])
+def test_verify_module(filename: str) -> None:
+    # upstream: none - Checks the Dafny proof surface.
+    # upstream-reason: verification.
+    run_dafny_verify(PROJECT / filename)
diff --git a/bench/utils/unlink/Unlink.dfy b/bench/utils/unlink/Unlink.dfy
new file mode 100644
index 00000000..7576783d
--- /dev/null
+++ b/bench/utils/unlink/Unlink.dfy
@@ -0,0 +1,75 @@
+include "../../core/BenchmarkItem.dfy"
+include "../../core/Utf8.dfy"
+include "UnlinkSchema.dfy"
+include "UnlinkSpec.dfy"
+include "UnlinkCore.dfy"
+include "UnlinkProof.dfy"
+
+module Unlink {
+  import BenchIO
+  import BenchWorld
+  import BenchItem
+  import CliTypes
+  import Utf8 = Utf8Semantics
+  import S = UnlinkSchema
+  import Core = UnlinkCore
+  import Spec = UnlinkSpec
+  import Proof = UnlinkProof
+  import opened CliExtern
+
+  class UnlinkBenchmarkItem extends BenchItem.BenchmarkItemTwostate<S.UnlinkCmdRaw> {
+    constructor() {}
+
+    method Name() returns (name: string) {
+      name := "unlink";
+    }
+
+    method Schema() returns (schema: CliTypes.CliSchema) {
+      schema := S.Schema();
+    }
+
+    method ParseConfig() returns (cfg: CliTypes.ParseConfig) {
+      cfg := S.ParserConfig();
+    }
+
+    method Decode(parsed: CliTypes.ParsedArgs) returns (raw: S.UnlinkCmdRaw) {
+      raw := S.Decode(parsed);
+    }
+
+    method FormatParseError(err: CliTypes.ParseError) returns (msg: BenchWorld.Bytes) {
+      msg := Spec.ParseErrorText(err);
+    }
+
+    method PlanParseFailure(
+      e: CliTypes.ParseError,
+      argv: seq<string>
+    ) returns (plan: CliTypes.CliPlan<S.UnlinkCmdRaw>)
+      decreases *
+    {
+      if 0 < e.tokenIndex && e.tokenIndex < |argv| {
+        var s := S.Schema();
+        var cfg := S.ParserConfig();
+        var result := Cli.Parse(argv[..e.tokenIndex], s, cfg);
+        match result {
+          case ParseSuccess(parsed) =>
+            var raw := S.Decode(parsed);
+            if raw.mode == S.ModeHelp || raw.mode == S.ModeVersion {
+              plan := CliTypes.CliRun(raw);
+              return;
+            }
+          case ParseFailure(_) =>
+        }
+      }
+      var msg := Spec.ParseErrorText(e);
+      plan := CliTypes.CliEarlyExit(1, [], msg);
+    }
+
+    method RunCore(raw: S.UnlinkCmdRaw, io: BenchIO.IO) returns (exit: int)
+      modifies io.fsRegion, io.stdoutRegion, io.stderrRegion
+      ensures Spec.Spec(raw, io, exit)
+    {
+      exit := Core.RunCore(raw, io);
+      Proof.CoreSummaryImpliesSpec(raw, io, exit);
+    }
+  }
+}
diff --git a/bench/utils/unlink/UnlinkCli.dfy b/bench/utils/unlink/UnlinkCli.dfy
new file mode 100644
index 00000000..d8a16305
--- /dev/null
+++ b/bench/utils/unlink/UnlinkCli.dfy
@@ -0,0 +1,20 @@
+include "Unlink.dfy"
+
+module UnlinkCli {
+  import BenchIO
+  import BenchItem
+  import Unlink
+
+  method {:main} Main(args: seq<string>)
+    modifies BenchIO.Process().Footprint()
+    decreases *
+  {
+    // Match the repository's .NET entry convention.
+    var effectiveArgs := if |args| > 0 && args[0] == "dotnet" then args[1..] else args;
+    var argv := ["unlink"] + effectiveArgs;
+    var io := BenchIO.Process();
+    var item := new Unlink.UnlinkBenchmarkItem();
+    var exit := BenchItem.RunMain(item, argv, io);
+    BenchIO.Exit(exit);
+  }
+}
diff --git a/bench/utils/unlink/UnlinkCore.dfy b/bench/utils/unlink/UnlinkCore.dfy
new file mode 100644
index 00000000..612de8a7
--- /dev/null
+++ b/bench/utils/unlink/UnlinkCore.dfy
@@ -0,0 +1,85 @@
+include "../../core/IO.dfy"
+include "UnlinkSchema.dfy"
+include "UnlinkSpec.dfy"
+
+module UnlinkCore {
+  import BenchIO
+  import Schema = UnlinkSchema
+  import Spec = UnlinkSpec
+  import C = IOContract
+  import Utf8 = Utf8Semantics
+
+  twostate predicate CoreSummary(raw: Schema.UnlinkCmdRaw, io: BenchIO.IO, exit: int)
+    reads io.Footprint()
+  {
+    if raw.mode == Schema.ModeHelp then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) + Spec.HelpTextSpec() &&
+      io.stderr() == old(io.stderr()) &&
+      exit == 0
+    else if raw.mode == Schema.ModeVersion then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) + Spec.VersionTextSpec() &&
+      io.stderr() == old(io.stderr()) &&
+      exit == 0
+    else if raw.mode != Schema.ModeRun then
+      match raw.mode
+      case ModeExtraOperand(operand) =>
+        io.fs() == old(io.fs()) &&
+        io.stdout() == old(io.stdout()) &&
+        io.stderr() == old(io.stderr()) +
+          Spec.ExtraOperandText(C.QuoteArgumentResult(Utf8.Encode(operand))) &&
+        exit == 1
+      case _ => false
+    else if |raw.operands| == 0 then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) &&
+      io.stderr() == old(io.stderr()) + Spec.MissingOperandText() &&
+      exit == 1
+    else
+      exists ok: bool, err: int ::
+        Spec.UnlinkResult(io, raw.operands[0], ok, err) &&
+        io.stdout() == old(io.stdout()) &&
+        (if ok then
+          io.stderr() == old(io.stderr()) && exit == 0
+        else
+          io.stderr() == old(io.stderr()) +
+            Spec.CannotUnlinkText(C.QuoteafPathResult(raw.operands[0]), C.CLocaleErrnoTextResult(err)) &&
+          exit == 1)
+  }
+
+  method RunCore(raw: Schema.UnlinkCmdRaw, io: BenchIO.IO) returns (exit: int)
+    modifies io.fsRegion, io.stdoutRegion, io.stderrRegion
+    ensures CoreSummary(raw, io, exit)
+  {
+    if raw.mode == Schema.ModeHelp {
+      io.AppendStdout(Spec.HelpTextSpec());
+      exit := 0;
+    } else if raw.mode == Schema.ModeVersion {
+      io.AppendStdout(Spec.VersionTextSpec());
+      exit := 0;
+    } else if raw.mode.ModeExtraOperand? {
+      var quotedOperand := io.QuoteArgument(Utf8.Encode(raw.mode.operand));
+      io.AppendStderr(Spec.ExtraOperandText(quotedOperand));
+      exit := 1;
+    } else if |raw.operands| == 0 {
+      io.AppendStderr(Spec.MissingOperandText());
+      exit := 1;
+    } else {
+      var ok, err := io.UnlinkPath(raw.operands[0]);
+      assert Spec.UnlinkResult(io, raw.operands[0], ok, err);
+
+      if ok {
+        exit := 0;
+      } else {
+        var reason := io.GetCLocaleErrnoText(err);
+        var quotedPath := io.QuoteafPath(raw.operands[0]);
+        io.AppendStderr(Spec.CannotUnlinkText(quotedPath, reason));
+        exit := 1;
+
+        assert C.GetCLocaleErrnoTextSpec(err, reason);
+        assert Spec.UnlinkResult(io, raw.operands[0], ok, err);
+      }
+    }
+  }
+}
diff --git a/bench/utils/unlink/UnlinkProof.dfy b/bench/utils/unlink/UnlinkProof.dfy
new file mode 100644
index 00000000..96101eae
--- /dev/null
+++ b/bench/utils/unlink/UnlinkProof.dfy
@@ -0,0 +1,17 @@
+include "UnlinkSpec.dfy"
+include "UnlinkCore.dfy"
+
+module UnlinkProof {
+  import BenchIO
+  import Schema = UnlinkSchema
+  import Core = UnlinkCore
+  import Spec = UnlinkSpec
+
+  twostate lemma CoreSummaryImpliesSpec(
+    raw: Schema.UnlinkCmdRaw, io: BenchIO.IO, exit: int)
+    requires Core.CoreSummary(raw, io, exit)
+    ensures Spec.Spec(raw, io, exit)
+  {
+    
+  }
+}
diff --git a/bench/utils/unlink/UnlinkSchema.dfy b/bench/utils/unlink/UnlinkSchema.dfy
new file mode 100644
index 00000000..d6c0068b
--- /dev/null
+++ b/bench/utils/unlink/UnlinkSchema.dfy
@@ -0,0 +1,64 @@
+include "../../core/CliTypes.dfy"
+
+module UnlinkSchema {
+  import CliTypes
+
+  datatype UnlinkMode = ModeRun | ModeHelp | ModeVersion | ModeExtraOperand(operand: string)
+
+  datatype UnlinkCmdRaw = UnlinkCmdRaw(
+    mode: UnlinkMode,
+    operands: seq<string>
+  )
+
+  method Schema() returns (schema: CliTypes.CliSchema)
+  {
+    schema := CliTypes.CliSchema([
+      CliTypes.OptionDecl("unlink.help", [], ["help"], CliTypes.NoArg),
+      CliTypes.OptionDecl("unlink.version", [], ["version"], CliTypes.NoArg)
+    ], true);
+  }
+
+  method ParserConfig() returns (cfg: CliTypes.ParseConfig)
+  {
+    cfg := CliTypes.ParseConfig(CliTypes.GNU_Permute, false, true, true);
+  }
+
+  method Decode(parsed: CliTypes.ParsedArgs) returns (raw: UnlinkCmdRaw)
+  {
+    var seenHelp := false;
+    var seenVersion := false;
+    var helpTokenIndex := -1;
+    var versionTokenIndex := -1;
+    var i := 0;
+    while i < |parsed.options|
+      decreases |parsed.options| - i
+    {
+      var option := parsed.options[i];
+
+      if option.key == "unlink.help" {
+        seenHelp := true;
+        if helpTokenIndex == -1 || option.tokenIndex < helpTokenIndex {
+          helpTokenIndex := option.tokenIndex;
+        }
+      }
+      if option.key == "unlink.version" {
+        seenVersion := true;
+        if versionTokenIndex == -1 || option.tokenIndex < versionTokenIndex {
+          versionTokenIndex := option.tokenIndex;
+        }
+      }
+
+      i := i + 1;
+    }
+    var mode := if seenHelp && (!seenVersion || helpTokenIndex <= versionTokenIndex) then
+        ModeHelp
+      else if seenVersion then
+        ModeVersion
+      else if |parsed.positionals| > 1 then
+        ModeExtraOperand(parsed.positionals[1])
+      else
+        ModeRun;
+
+    raw := UnlinkCmdRaw(mode, parsed.positionals);
+  }
+}
diff --git a/bench/utils/unlink/UnlinkSpec.dfy b/bench/utils/unlink/UnlinkSpec.dfy
new file mode 100644
index 00000000..a608d381
--- /dev/null
+++ b/bench/utils/unlink/UnlinkSpec.dfy
@@ -0,0 +1,163 @@
+include "UnlinkSchema.dfy"
+include "../../core/IO.dfy"
+include "../../core/Utf8.dfy"
+include "../../core/CliModel.dfy"
+
+module UnlinkSpec {
+  import BenchIO
+  import BenchWorld
+  import CliTypes
+  import Schema = UnlinkSchema
+  import Utf8 = Utf8Semantics
+  import CliModel
+  import C = IOContract
+
+  function HelpTextSpec(): BenchWorld.Bytes
+  {
+    "Usage: unlink FILE\n"
+    + "  or:  unlink OPTION\n"
+    + "Call the unlink function to remove the specified FILE.\n"
+    + "\n"
+    + "      --help\n"
+    + "         display this help and exit\n"
+    + "      --version\n"
+    + "         output version information and exit\n"
+    + "\n"
+    + "Report bugs to: bug-coreutils@gnu.org\n"
+    + "GNU coreutils home page: <https://www.gnu.org/software/coreutils/>\n"
+    + "General help using GNU software: <https://www.gnu.org/gethelp/>\n"
+    + "Report any translation bugs to <https://translationproject.org/team/>\n"
+    + "Full documentation <https://www.gnu.org/software/coreutils/unlink>\n"
+    + "or available locally via: info '(coreutils) unlink invocation'\n"
+  }
+
+  function VersionTextSpec(): BenchWorld.Bytes
+  {
+    "unlink (GNU coreutils) 9.10.13-2cf49\n"
+    + "Copyright (C) 2026 Free Software Foundation, Inc.\n"
+    + "License GPLv3+: GNU GPL version 3 or later <https://gnu.org/licenses/gpl.html>.\n"
+    + "This is free software: you are free to change and redistribute it.\n"
+    + "There is NO WARRANTY, to the extent permitted by law.\n"
+    + "\n"
+    + "Written by Michael Stone.\n"
+  }
+
+
+  function LongOptionName(token: string): string
+  {
+    var eq := CliModel.FindChar(token, '=');
+    var name := if eq >= 0 then token[..eq] else token;
+    if |name| > 2 && CliModel.HasPrefix(name, "--") then
+      var abbreviation := name[2..];
+      if CliModel.HasPrefix("help", abbreviation) then "--help"
+      else if CliModel.HasPrefix("version", abbreviation) then "--version"
+      else name
+    else name
+  }
+
+  function ParseErrorText(err: CliTypes.ParseError): BenchWorld.Bytes
+  {
+    var text := if err.kind == CliTypes.UnknownOption then
+        if |err.rawToken| > 2 && err.rawToken[0] == '-' && err.rawToken[1] == '-' then
+          "unlink: unrecognized option '" + err.rawToken + "'\n" +
+          "Try 'unlink --help' for more information.\n"
+        else if |err.rawToken| > 1 && err.rawToken[0] == '-' then
+          "unlink: invalid option -- '" + [err.rawToken[1]] + "'\n" +
+          "Try 'unlink --help' for more information.\n"
+        else
+          "unlink: invalid option\nTry 'unlink --help' for more information.\n"
+      else if err.kind == CliTypes.UnexpectedValue then
+        "unlink: option '" + LongOptionName(err.rawToken) +
+        "' doesn't allow an argument\n" +
+        "Try 'unlink --help' for more information.\n"
+      else if err.kind == CliTypes.Ambiguous then
+        "unlink: option '" + err.rawToken + "' is ambiguous\n" +
+        "Try 'unlink --help' for more information.\n"
+      else
+        "unlink: " +
+        (if err.kind == CliTypes.MissingValue
+        then "missing option value"
+        else "parse error") +
+        " at token '" + err.rawToken + "'\n";
+    Utf8.Encode(text)
+  }
+
+  twostate predicate UnlinkResult(
+    io: BenchIO.IO,
+    path: BenchWorld.Path,
+    ok: bool,
+    err: int
+  )
+    reads io.fsRegion, io.nowRegion, io.trustedFilesystemRegion
+  {
+    C.UnlinkPathSpec(
+      old(io.fs()),
+      old(io.now()),
+      old(io.trustedFilesystem()),
+      io.fs(),
+      path,
+      ok,
+      err
+    )
+  }
+
+  function MissingOperandText(): BenchWorld.Bytes
+  {
+    "unlink: missing operand\n"
+    + "Try 'unlink --help' for more information.\n"
+  }
+
+  function ExtraOperandText(quotedOperand: BenchWorld.Bytes): BenchWorld.Bytes
+  {
+    "unlink: extra operand " + quotedOperand + "\n"
+    + "Try 'unlink --help' for more information.\n"
+  }
+
+  function CannotUnlinkText(
+    quotedPath: BenchWorld.Bytes,
+    reason: string
+  ): BenchWorld.Bytes
+  {
+    "unlink: cannot unlink " + quotedPath + ": "
+    + Utf8.Encode(reason) + "\n"
+  }
+
+  twostate predicate Spec(raw: Schema.UnlinkCmdRaw, io: BenchIO.IO, exit: int)
+    reads io.Footprint()
+  {
+    if raw.mode == Schema.ModeHelp then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) + HelpTextSpec() &&
+      io.stderr() == old(io.stderr()) &&
+      exit == 0
+    else if raw.mode == Schema.ModeVersion then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) + VersionTextSpec() &&
+      io.stderr() == old(io.stderr()) &&
+      exit == 0
+    else if raw.mode != Schema.ModeRun then
+      match raw.mode
+      case ModeExtraOperand(operand) =>
+        io.fs() == old(io.fs()) &&
+        io.stdout() == old(io.stdout()) &&
+        io.stderr() == old(io.stderr()) +
+          ExtraOperandText(C.QuoteArgumentResult(Utf8.Encode(operand))) &&
+        exit == 1
+      case _ => false
+    else if |raw.operands| == 0 then
+      io.fs() == old(io.fs()) &&
+      io.stdout() == old(io.stdout()) &&
+      io.stderr() == old(io.stderr()) + MissingOperandText() &&
+      exit == 1
+    else
+      exists ok: bool, err: int ::
+        UnlinkResult(io, raw.operands[0], ok, err) &&
+        io.stdout() == old(io.stdout()) &&
+        (if ok then
+          io.stderr() == old(io.stderr()) && exit == 0
+        else
+          io.stderr() == old(io.stderr()) +
+            CannotUnlinkText(C.QuoteafPathResult(raw.operands[0]), C.CLocaleErrnoTextResult(err)) &&
+          exit == 1)
+  }
+}
diff --git a/bench/utils/unlink/benchmark.yaml b/bench/utils/unlink/benchmark.yaml
new file mode 100644
index 00000000..ed18d234
--- /dev/null
+++ b/bench/utils/unlink/benchmark.yaml
@@ -0,0 +1,8 @@
+schema_version: benchmark.definition.v2
+task_id: "unlink"
+kind: coreutils
+source:
+  status: verified
+  name: GNU coreutils unlink
+  url: https://www.gnu.org/software/coreutils/
+  license: GPL-3.0-or-later
diff --git a/bench/utils/unlink/dfyconfig.toml b/bench/utils/unlink/dfyconfig.toml
new file mode 100644
index 00000000..e36375d0
--- /dev/null
+++ b/bench/utils/unlink/dfyconfig.toml
@@ -0,0 +1,6 @@
+includes = ["UnlinkCli.dfy"]
+
+[options]
+target = "cs"
+no-verify = true
+standard-libraries = false
diff --git a/bench/utils/unlink/unlink.md b/bench/utils/unlink/unlink.md
new file mode 100644
index 00000000..14f48d84
--- /dev/null
+++ b/bench/utils/unlink/unlink.md
@@ -0,0 +1,52 @@
+# unlink NL Specification
+
+Source:
+- `coreutils/doc/coreutils.texi`
+- `@node unlink invocation`
+- Source line range: 11114-11139
+- Implementation: `coreutils/src/unlink.c` at submodule commit
+  `2cf491412c199e2211880ec3f4ba387026638a33`
+- License: GPL-3.0-or-later
+
+This file summarizes the upstream GNU `unlink` behavior relevant to the benchmark.
+
+## `unlink`: Remove a file name
+
+`unlink` removes one specified file name using the system's `unlink` operation.
+It is a smaller interface than `rm`: it takes a single file name and does not
+offer recursive or interactive removal.
+
+```text
+unlink filename
+```
+
+Removing a symbolic link removes the link itself, leaving its target in place.
+If a file has other hard-link names, those names remain usable. GNU `unlink`
+does not remove directories.
+
+The command accepts `--help` and `--version`. To remove a name beginning with
+`-`, prefix it with `./`; for example, `unlink ./--help` removes the file named
+`--help` instead of displaying help.
+
+### Benchmark-Supported Behavior
+
+The benchmark handles one pathname, including regular files and symbolic links,
+plus `--help`, `--version`, `--`, and operand, option, and deletion errors.
+No options are excluded by `IO.dfy`.
+
+### Scope and model
+
+- **Input and environment:** Finite arguments, long-option abbreviations, Linux
+  filesystem, current user permissions, and C-locale diagnostics; stdin is unused.
+- **Observation:** Output streams, exit status, and modeled filesystem. Help,
+  version, and operand errors leave files unchanged. A failed `UnlinkPathSpec`
+  does not guarantee filesystem preservation; maintainer review is pending.
+- **Trusted API:** Shared parser, `UnlinkPathSpec`, errno text, argument/path quoting, and stream append
+  contracts in `bench/core` revision `4ac0d9b34816c54c822bd9870794aafae1df3c13`.
+- **Proof:** `Unlink.RunCore` ensures `UnlinkSpec.Spec` through `UnlinkProof`.
+  `Decode` terminates; whole-process termination is not proved.
+
+### Exit Status
+
+The supported command exits with status 0 after a successful removal or a help
+or version request. Operand, option, and deletion errors exit with status 1.
diff --git a/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs b/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs
index 61485324..f8776a0f 100644
--- a/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs
+++ b/tools/coreutils_fuzzer/src/fuzz/input/generators/mod.rs
@@ -33,4 +33,5 @@ pub(crate) mod touch;
 pub(crate) mod tr;
 pub(crate) mod r#true;
 pub(crate) mod uniq;
+pub(crate) mod unlink;
 pub(crate) mod wc;
diff --git a/tools/coreutils_fuzzer/src/fuzz/input/generators/unlink.rs b/tools/coreutils_fuzzer/src/fuzz/input/generators/unlink.rs
new file mode 100644
index 00000000..e8380e72
--- /dev/null
+++ b/tools/coreutils_fuzzer/src/fuzz/input/generators/unlink.rs
@@ -0,0 +1,87 @@
+use super::super::pattern::{Alternative, ArgvPattern, Atom, Element, OperandSource, OptionChoice};
+use super::super::PatternInputGenerator;
+use super::super::{fixtures, support};
+use crate::fuzz::{DirSpec, FileSpec, GeneratedCase, HardlinkSpec, SymlinkSpec};
+use std::path::PathBuf;
+
+const HELP_OR_VERSION: Atom = Atom::Option(OptionChoice::available(&["--help", "--version"]));
+const TARGET: Atom = Atom::Operand(OperandSource::Target {
+    existing_percent: 70,
+});
+
+static ARGV_PATTERN: ArgvPattern = ArgvPattern::new(&[
+    Alternative::new(&[
+        Element::repeated(0, 2, HELP_OR_VERSION),
+        Element::up_to_budget(0, TARGET),
+    ]),
+    Alternative::new(&[
+        Element::once(TARGET),
+        Element::repeated(1, 2, HELP_OR_VERSION),
+        Element::up_to_budget(0, TARGET),
+    ]),
+]);
+
+pub(crate) static GENERATOR: PatternInputGenerator =
+    PatternInputGenerator::patterned(&ARGV_PATTERN, scenario_case);
+
+pub(super) fn scenario_case(iteration: usize) -> Option<GeneratedCase> {
+    let mut fixture = fixtures::basic_fixture();
+    let args = match iteration {
+        0 => vec!["a.txt"],
+        1 => vec!["a-link"],
+        2 => {
+            fixture.symlinks.push(SymlinkSpec {
+                relative_path: PathBuf::from("dangling"),
+                target: PathBuf::from("missing.txt"),
+            });
+            vec!["dangling"]
+        }
+        3 => {
+            fixture.hardlinks.push(HardlinkSpec {
+                relative_path: PathBuf::from("alias"),
+                source_relative_path: PathBuf::from("a.txt"),
+            });
+            vec!["alias"]
+        }
+        4 => vec![],
+        5 => vec!["a.txt", "b.txt"],
+        6 => vec!["missing.txt"],
+        7 => vec![""],
+        8 => vec!["dir"],
+        9 => vec!["--help", "--version"],
+        10 => vec!["--version", "--help"],
+        11 => vec!["--help", "--bad"],
+        12 => vec!["--bad", "--help"],
+        13 => {
+            fixture.files.push(FileSpec {
+                relative_path: PathBuf::from("--help"),
+                bytes: b"keep unless explicitly unlinked\n".to_vec(),
+                mode: 0o644,
+            });
+            vec!["--", "--help"]
+        }
+        14 => vec!["--help=value"],
+        15 => vec!["-x"],
+        16 => vec!["--help", "a.txt"],
+        17 => vec!["a.txt", "--help"],
+        18 => vec!["a.txt", "--help", "b.txt"],
+        19 => vec!["--version", "a.txt"],
+        20 => vec!["a.txt", "--version"],
+        21 => vec!["a.txt", "--version", "b.txt"],
+        22 => vec!["--thisoptiondoesnotexist"],
+        23 => {
+            fixture.directories.push(DirSpec {
+                relative_path: PathBuf::from("blocked"),
+                mode: 0o555,
+            });
+            fixture.files.push(FileSpec {
+                relative_path: PathBuf::from("blocked/target"),
+                bytes: b"keep\n".to_vec(),
+                mode: 0o644,
+            });
+            vec!["blocked/target"]
+        }
+        _ => return None,
+    };
+    Some(support::case(args, fixture, b""))
+}
diff --git a/tools/coreutils_fuzzer/src/utils/capabilities.rs b/tools/coreutils_fuzzer/src/utils/capabilities.rs
index c10a8f23..a9e9bc2b 100644
--- a/tools/coreutils_fuzzer/src/utils/capabilities.rs
+++ b/tools/coreutils_fuzzer/src/utils/capabilities.rs
@@ -165,6 +165,7 @@ pub(crate) static UTILITY_CAPABILITIES: &[UtilityCapability] = &[
     },
     capability!("tr", tr),
     capability!("true", r#true),
+    capability!("unlink", unlink),
     UtilityCapability {
         path_operand_policy: PathOperandPolicy::First,
         stdin_policy: StdinPolicy::Uniq,
@@ -293,7 +294,7 @@ mod tests {
             patterned,
             BTreeSet::from([
                 "cat", "chmod", "comm", "csplit", "cut", "du", "expand", "head", "ln", "ls", "mv",
-                "nl", "paste", "readlink", "stat", "tac", "tail", "touch", "uniq", "wc",
+                "nl", "paste", "readlink", "stat", "tac", "tail", "touch", "uniq", "unlink", "wc",
             ])
         );
     }